Nuprl Lemma : is-half-cube-sub-cube
∀[k:ℕ]. ∀h,c:ℚCube(k). (rat-sub-cube(k;h;c)) supposing ((↑is-half-cube(k;h;c)) and (↑Inhabited(c)))
Proof
Definitions occuring in Statement :
inhabited-rat-cube: Inhabited(c),
is-half-cube: is-half-cube(k;h;c),
rat-sub-cube: rat-sub-cube(k;a;b),
rational-cube: ℚCube(k),
nat: ℕ,
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
rational-cube: ℚCube(k),
implies: P ⇒ Q,
rat-sub-cube: rat-sub-cube(k;a;b),
nat: ℕ,
prop: ℙ,
iff: P ⇐⇒ Q,
and: P ∧ Q
Lemmas referenced :
assert_witness,
inhabited-rat-interval_wf,
is-half-interval_wf,
is-half-interval-sub-interval,
int_seg_wf,
istype-assert,
rational-cube_wf,
istype-nat,
iff_weakening_uiff,
assert_wf,
inhabited-rat-cube_wf,
assert-inhabited-rat-cube,
is-half-cube_wf,
assert-is-half-cube
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
introduction,
sqequalRule,
sqequalHypSubstitution,
lambdaEquality_alt,
dependent_functionElimination,
thin,
hypothesisEquality,
extract_by_obid,
isectElimination,
applyEquality,
hypothesis,
independent_functionElimination,
functionIsTypeImplies,
inhabitedIsType,
rename,
independent_isectElimination,
because_Cache,
functionIsType,
universeIsType,
natural_numberEquality,
setElimination,
functionEquality,
productElimination
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}h,c:\mBbbQ{}Cube(k). (rat-sub-cube(k;h;c)) supposing ((\muparrow{}is-half-cube(k;h;c)) and (\muparrow{}Inhabited(c)))
Date html generated:
2020_05_20-AM-09_18_31
Last ObjectModification:
2019_11_14-PM-08_16_42
Theory : rationals
Home
Index