### Nuprl Lemma : rmin-i-member

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

Proof

Definitions occuring in Statement :  i-member: `r ∈ I` interval: `Interval` rmin: `rmin(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` member: `t ∈ T` iff: `P `⇐⇒` Q` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` or: `P ∨ Q` prop: `ℙ` true: `True`
Lemmas referenced :  rmin_ub rmin_lb rleq_wf and_wf real_wf rmin_strict_ub rless_wf rmin_strict_lb true_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin unionElimination sqequalRule cut lemma_by_obid dependent_functionElimination hypothesisEquality because_Cache independent_functionElimination hypothesis independent_pairFormation isectElimination independent_isectElimination inlFormation natural_numberEquality

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

Date html generated: 2016_05_18-AM-08_47_53
Last ObjectModification: 2015_12_27-PM-11_47_02

Theory : reals

Home Index