Nuprl Lemma : rmin-rmax-absorption-strong

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


Proof




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

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



Date html generated: 2017_10_03-AM-08_22_48
Last ObjectModification: 2017_07_28-AM-07_22_33

Theory : reals


Home Index