Nuprl Lemma : rmin_lb

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


Proof




Definitions occuring in Statement :  rleq: x ≤ y rmin: rmin(x;y) real: uimplies: supposing a uall: [x:A]. B[x] or: P ∨ Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a or: P ∨ Q and: P ∧ Q guard: {T} 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:
Lemmas referenced :  rmin-rleq rleq_transitivity rmin_wf less_than'_wf rsub_wf real_wf nat_plus_wf or_wf rleq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality unionElimination productElimination hypothesis independent_isectElimination sqequalRule lambdaEquality dependent_functionElimination independent_pairEquality because_Cache applyEquality setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination

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



Date html generated: 2016_05_18-AM-07_16_55
Last ObjectModification: 2015_12_28-AM-00_44_03

Theory : reals


Home Index