Nuprl Lemma : strict-upper-bound_functionality

A:Set(ℝ). ∀b,c:ℝ.  {A <  A < c} supposing b ≤ c


Proof




Definitions occuring in Statement :  strict-upper-bound: A < b rset: Set(ℝ) rleq: x ≤ y real: uimplies: supposing a guard: {T} all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  strict-upper-bound: A < b guard: {T} all: x:A. B[x] uimplies: supposing a member: t ∈ T rleq: x ≤ y rnonneg: rnonneg(x) le: A ≤ B and: P ∧ Q not: ¬A implies:  Q false: False uall: [x:A]. B[x] subtype_rel: A ⊆B real: prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q rge: x ≥ y
Lemmas referenced :  less_than'_wf rsub_wf real_wf nat_plus_wf rset-member_wf all_wf rless_wf rleq_wf rset_wf rless_functionality_wrt_implies rleq_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation isect_memberFormation cut introduction sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality productElimination independent_pairEquality voidElimination lemma_by_obid isectElimination applyEquality hypothesis setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality because_Cache independent_isectElimination independent_functionElimination

Latex:
\mforall{}A:Set(\mBbbR{}).  \mforall{}b,c:\mBbbR{}.    \{A  <  b  {}\mRightarrow{}  A  <  c\}  supposing  b  \mleq{}  c



Date html generated: 2016_05_18-AM-08_09_17
Last ObjectModification: 2015_12_28-AM-01_15_41

Theory : reals


Home Index