Nuprl Lemma : rmin-assoc

[x,y,z:ℝ].  (rmin(rmin(x;y);z) rmin(x;rmin(y;z)))


Proof




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

Latex:
\mforall{}[x,y,z:\mBbbR{}].    (rmin(rmin(x;y);z)  =  rmin(x;rmin(y;z)))



Date html generated: 2017_10_03-AM-08_22_29
Last ObjectModification: 2017_07_28-AM-07_22_22

Theory : reals


Home Index