Nuprl Lemma : rmin-rleq

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


Proof




Definitions occuring in Statement :  rleq: x ≤ y rmin: rmin(x;y) real: uall: [x:A]. B[x] and: P ∧ Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q cand: c∧ B rleq: x ≤ y rnonneg: rnonneg(x) all: x:A. B[x] le: A ≤ B not: ¬A implies:  Q false: False subtype_rel: A ⊆B real: prop: uimplies: supposing a rge: x ≥ y uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  less_than'_wf rsub_wf rmin_wf real_wf nat_plus_wf rminus_wf rmax_wf rminus_functionality_wrt_rleq rleq-rmax rleq_functionality rmin-req-rminus-rmax req_weakening req_inversion rminus-rminus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation hypothesis sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality because_Cache lemma_by_obid isectElimination applyEquality setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination independent_isectElimination

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



Date html generated: 2016_05_18-AM-07_16_35
Last ObjectModification: 2015_12_28-AM-00_43_19

Theory : reals


Home Index