Nuprl Lemma : upper-rc-face_wf
∀[k:ℕ]. ∀[c:ℚCube(k)]. ∀[j:ℕk]. (upper-rc-face(c;j) ∈ ℚCube(k))
Proof
Definitions occuring in Statement :
upper-rc-face: upper-rc-face(c;j),
rational-cube: ℚCube(k),
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
natural_number: $n
Definitions unfolded in proof :
nat: ℕ,
pi2: snd(t),
rational-interval: ℚInterval,
implies: P ⇒ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
rational-cube: ℚCube(k),
upper-rc-face: upper-rc-face(c;j),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
istype-nat,
rational-cube_wf,
int_seg_wf,
rat-point-interval_wf,
rational-interval_wf,
eq_int_wf,
ifthenelse_wf
Rules used in proof :
isectIsTypeImplies,
isect_memberEquality_alt,
natural_numberEquality,
universeIsType,
axiomEquality,
independent_functionElimination,
dependent_functionElimination,
equalitySymmetry,
equalityTransitivity,
equalityIstype,
sqequalRule,
productElimination,
lambdaFormation_alt,
inhabitedIsType,
applyEquality,
hypothesis,
hypothesisEquality,
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
lambdaEquality_alt,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[c:\mBbbQ{}Cube(k)]. \mforall{}[j:\mBbbN{}k]. (upper-rc-face(c;j) \mmember{} \mBbbQ{}Cube(k))
Date html generated:
2019_10_29-AM-07_56_37
Last ObjectModification:
2019_10_17-PM-03_34_46
Theory : rationals
Home
Index