Nuprl Lemma : rmax_functionality

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


Definitions occuring in Statement :  rmax: rmax(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 rmax_wf req_witness req_wf real_wf bdd-diff_functionality rmax_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{}].    (rmax(x1;y1)  =  rmax(x2;y2))  supposing  ((x1  =  x2)  and  (y1  =  y2))

Date html generated: 2016_05_18-AM-06_59_01
Last ObjectModification: 2015_12_28-AM-00_32_12

Theory : reals

Home Index