Nuprl Lemma : rmin_functionality

[x1,x2,y1,y2:ℝ].  (rmin(x1;y1) rmin(x2;y2)) supposing ((x1 x2) and (y1 y2))


Definitions occuring in Statement :  rmin: rmin(x;y) req: y real: uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) implies:  Q prop: subtype_rel: A ⊆B real: all: x:A. B[x] iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  req-iff-bdd-diff rmin_wf req_witness req_wf real_wf bdd-diff_functionality rmin_functionality_wrt_bdd-diff bdd-diff_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination independent_functionElimination sqequalRule isect_memberEquality because_Cache equalityTransitivity equalitySymmetry applyEquality lambdaEquality setElimination rename dependent_functionElimination

\mforall{}[x1,x2,y1,y2:\mBbbR{}].    (rmin(x1;y1)  =  rmin(x2;y2))  supposing  ((x1  =  x2)  and  (y1  =  y2))

Date html generated: 2016_05_18-AM-06_59_22
Last ObjectModification: 2015_12_28-AM-00_32_30

Theory : reals

Home Index