Nuprl Lemma : rmin_functionality_wrt_rleq
∀[x1,x2,y1,y2:ℝ]. (rmin(x1;y1) ≤ rmin(x2;y2)) supposing ((y1 ≤ y2) and (x1 ≤ x2))
Proof
Definitions occuring in Statement :
rleq: x ≤ y,
rmin: rmin(x;y),
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
guard: {T},
prop: ℙ,
le: A ≤ B,
rnonneg: rnonneg(x),
rleq: x ≤ y,
cand: A c∧ B,
implies: P ⇒ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rleq_transitivity,
rmin-rleq,
real_wf,
rleq_wf,
le_witness_for_triv,
rmin_wf,
rmin_ub
Rules used in proof :
isectIsTypeImplies,
isect_memberEquality_alt,
universeIsType,
inhabitedIsType,
functionIsTypeImplies,
independent_isectElimination,
equalitySymmetry,
equalityTransitivity,
lambdaEquality_alt,
sqequalRule,
independent_pairFormation,
independent_functionElimination,
productElimination,
hypothesis,
isectElimination,
hypothesisEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[x1,x2,y1,y2:\mBbbR{}]. (rmin(x1;y1) \mleq{} rmin(x2;y2)) supposing ((y1 \mleq{} y2) and (x1 \mleq{} x2))
Date html generated:
2019_11_06-PM-00_27_27
Last ObjectModification:
2019_11_05-PM-00_09_00
Theory : reals
Home
Index