### Nuprl Lemma : rmax-i-member

`∀I:Interval. ∀a,b:ℝ.  ((a ∈ I) `` (b ∈ I) `` (rmax(a;b) ∈ I))`

Proof

Definitions occuring in Statement :  i-member: `r ∈ I` interval: `Interval` rmax: `rmax(x;y)` real: `ℝ` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` interval: `Interval` i-member: `r ∈ I` implies: `P `` Q` and: `P ∧ Q` cand: `A c∧ B` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` or: `P ∨ Q` prop: `ℙ` uiff: `uiff(P;Q)` iff: `P `⇐⇒` Q` true: `True`
Lemmas referenced :  rmax_ub rleq_wf rmax_lb and_wf real_wf rmax_strict_ub rless_wf rmax_strict_lb true_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin unionElimination sqequalRule cut lemma_by_obid isectElimination hypothesisEquality because_Cache independent_isectElimination inlFormation hypothesis independent_pairFormation dependent_functionElimination independent_functionElimination natural_numberEquality

Latex:
\mforall{}I:Interval.  \mforall{}a,b:\mBbbR{}.    ((a  \mmember{}  I)  {}\mRightarrow{}  (b  \mmember{}  I)  {}\mRightarrow{}  (rmax(a;b)  \mmember{}  I))

Date html generated: 2016_05_18-AM-08_48_02
Last ObjectModification: 2015_12_27-PM-11_46_43

Theory : reals

Home Index