Nuprl Lemma : rmin-rmax-absorption

b,a:ℝ.  (rmin(b;rmax(b;a)) b)


Proof




Definitions occuring in Statement :  rmin: rmin(x;y) rmax: rmax(x;y) req: y real: all: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T squash: T uall: [x:A]. B[x] prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q
Lemmas referenced :  real_wf req_weakening iff_weakening_equal rmin-rmax-absorption-strong true_wf squash_wf req_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination lemma_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache dependent_functionElimination natural_numberEquality sqequalRule imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination

Latex:
\mforall{}b,a:\mBbbR{}.    (rmin(b;rmax(b;a))  =  b)



Date html generated: 2016_05_18-AM-06_59_52
Last ObjectModification: 2016_01_13-PM-04_28_26

Theory : reals


Home Index