Nuprl Lemma : rmin_functionality

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

Proof

Definitions occuring in Statement :  rmin: `rmin(x;y)` req: `x = y` real: `ℝ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` real: `ℝ` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` rev_implies: `P `` 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

Latex:
\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