### Nuprl Lemma : rmin-req

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

Proof

Definitions occuring in Statement :  rleq: x ≤ y 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 implies:  Q prop: uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q
Lemmas referenced :  rmin-req-rminus-rmax req_inversion iff_weakening_equal rminus-rminus-eq true_wf squash_wf req_wf rminus_functionality req_functionality req_weakening rmax_wf real_wf rleq_wf rmin_wf req_witness rminus-reverses-rleq rminus_wf rmax-req
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination independent_functionElimination sqequalRule isect_memberEquality because_Cache equalityTransitivity equalitySymmetry productElimination applyEquality lambdaEquality imageElimination natural_numberEquality imageMemberEquality baseClosed universeEquality

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

Date html generated: 2016_05_18-AM-07_15_43
Last ObjectModification: 2016_01_17-AM-01_53_44

Theory : reals

Home Index