### Nuprl Lemma : rpositive-rmax

`∀x,y:ℝ.  (rpositive(rmax(x;y)) `⇐⇒` rpositive(x) ∨ rpositive(y))`

Proof

Definitions occuring in Statement :  rpositive: `rpositive(x)` rmax: `rmax(x;y)` real: `ℝ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` real: `ℝ` rev_implies: `P `` Q` rpositive: `rpositive(x)` sq_exists: `∃x:{A| B[x]}` rmax: `rmax(x;y)` or: `P ∨ Q` guard: `{T}`
Lemmas referenced :  rpositive_wf rmax_wf real_wf or_wf imax_strict_ub less_than_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality lambdaEquality setElimination rename sqequalRule dependent_functionElimination natural_numberEquality productElimination independent_functionElimination unionElimination inlFormation dependent_set_memberFormation inrFormation introduction dependent_set_memberEquality because_Cache

Latex:
\mforall{}x,y:\mBbbR{}.    (rpositive(rmax(x;y))  \mLeftarrow{}{}\mRightarrow{}  rpositive(x)  \mvee{}  rpositive(y))

Date html generated: 2016_05_18-AM-07_01_02
Last ObjectModification: 2015_12_28-AM-00_33_34

Theory : reals

Home Index