Nuprl Lemma : rmin-classical-cases
∀a,b:ℝ. (¬¬((rmin(a;b) = a) ∨ (rmin(a;b) = b)))
Proof
Definitions occuring in Statement :
rmin: rmin(x;y),
req: x = y,
real: ℝ,
all: ∀x:A. B[x],
not: ¬A,
or: P ∨ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
false: False,
or: P ∨ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
uimplies: b supposing a,
stable: Stable{P},
guard: {T}
Lemmas referenced :
req_wf,
rmin_wf,
istype-void,
real_wf,
stable__false,
false_wf,
rless_wf,
not_wf,
not-rless,
minimal-double-negation-hyp-elim,
minimal-not-not-excluded-middle,
rmin-req2,
rleq_weakening_rless,
rmin-req
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
thin,
because_Cache,
hypothesis,
sqequalHypSubstitution,
independent_functionElimination,
voidElimination,
sqequalRule,
functionIsType,
unionIsType,
universeIsType,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
inhabitedIsType,
unionEquality,
functionEquality,
independent_isectElimination,
unionElimination,
inlFormation_alt,
inrFormation_alt
Latex:
\mforall{}a,b:\mBbbR{}. (\mneg{}\mneg{}((rmin(a;b) = a) \mvee{} (rmin(a;b) = b)))
Date html generated:
2019_10_29-AM-09_38_40
Last ObjectModification:
2019_07_29-PM-03_11_24
Theory : reals
Home
Index