Nuprl Lemma : rless-cases-sq
∀x:ℝ. ∀y:{y:ℝ| x < y} . ∀z:ℝ. ((x < z) ∨ (z < y))
Proof
Definitions occuring in Statement :
rless: x < y,
real: ℝ,
all: ∀x:A. B[x],
or: P ∨ Q,
set: {x:A| B[x]}
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
rless-cases,
rlessw_wf,
rless_wf,
real_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
setElimination,
rename,
hypothesis,
independent_functionElimination,
inhabitedIsType,
setIsType,
universeIsType,
isectElimination
Latex:
\mforall{}x:\mBbbR{}. \mforall{}y:\{y:\mBbbR{}| x < y\} . \mforall{}z:\mBbbR{}. ((x < z) \mvee{} (z < y))
Date html generated:
2019_10_29-AM-10_04_36
Last ObjectModification:
2019_10_02-PM-06_34_31
Theory : reals
Home
Index