Nuprl Lemma : rat-cube-face-self
∀[k:ℕ]. ∀c:ℚCube(k). c ≤ c
Proof
Definitions occuring in Statement :
rat-cube-face: c ≤ d,
rational-cube: ℚCube(k),
nat: ℕ,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x]
Definitions unfolded in proof :
nat: ℕ,
rational-cube: ℚCube(k),
member: t ∈ T,
rat-cube-face: c ≤ d,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x]
Lemmas referenced :
istype-nat,
rational-cube_wf,
int_seg_wf,
rat-interval-face-self
Rules used in proof :
rename,
setElimination,
natural_numberEquality,
isectElimination,
universeIsType,
hypothesis,
hypothesisEquality,
applyEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation_alt,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}c:\mBbbQ{}Cube(k). c \mleq{} c
Date html generated:
2019_10_29-AM-07_49_39
Last ObjectModification:
2019_10_18-PM-01_03_33
Theory : rationals
Home
Index