Nuprl Lemma : half-cube-dimension
∀[k:ℕ]. ∀[c:{c:ℚCube(k)| ↑Inhabited(c)} ]. ∀[h:ℚCube(k)]. ((↑is-half-cube(k;h;c)) ⇒ (dim(h) = dim(c) ∈ ℤ))
Proof
Definitions occuring in Statement :
rat-cube-dimension: dim(c),
inhabited-rat-cube: Inhabited(c),
is-half-cube: is-half-cube(k;h;c),
rational-cube: ℚCube(k),
nat: ℕ,
assert: ↑b,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
rat-cube-dimension: dim(c),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
iff: P ⇐⇒ Q,
true: True,
rev_implies: P ⇐ Q,
sq_type: SQType(T),
all: ∀x:A. B[x],
guard: {T},
rational-cube: ℚCube(k),
nat: ℕ,
rational-interval: ℚInterval,
rat-interval-dimension: dim(I),
is-half-interval: is-half-interval(I;J),
or: P ∨ Q,
squash: ↓T,
prop: ℙ,
rev_uimplies: rev_uimplies(P;Q),
subtype_rel: A ⊆r B,
int_seg: {i..j-},
lelt: i ≤ j < k,
le: A ≤ B,
bfalse: ff,
band: p ∧b q,
bool: 𝔹,
unit: Unit,
it: ⋅,
exists: ∃x:A. B[x],
bnot: ¬bb,
false: False,
so_lambda: λ2x.t[x],
so_apply: x[s],
not: ¬A,
inhabited-rat-interval: Inhabited(I),
qavg: qavg(a;b),
qless: r < s,
grp_lt: a < b,
set_lt: a <p b,
set_blt: a <b b,
infix_ap: x f y,
set_le: ≤b,
pi2: snd(t),
oset_of_ocmon: g↓oset,
dset_of_mon: g↓set,
grp_le: ≤b,
pi1: fst(t),
qadd_grp: <ℚ+>,
q_le: q_le(r;s),
callbyvalueall: callbyvalueall,
evalall: evalall(t),
bor: p ∨bq,
qpositive: qpositive(r),
qsub: r - s,
qadd: r + s,
qmul: r * s,
lt_int: i <z j,
qeq: qeq(r;s),
eq_int: (i =z j)
Lemmas referenced :
assert-is-half-cube,
subtype_base_sq,
bool_wf,
bool_subtype_base,
iff_imp_equal_bool,
inhabited-rat-cube_wf,
btrue_wf,
istype-true,
istype-assert,
is-half-cube_wf,
int_seg_wf,
ifthenelse_wf,
squash_wf,
true_wf,
istype-universe,
q_less_wf,
qless-qavg-iff-1,
qless_wf,
qavg_wf,
rationals_wf,
subtype_rel_self,
iff_weakening_equal,
assert-q_less-eq,
qavg-qless-iff-1,
assert_wf,
bor_wf,
qeq_wf2,
bool_cases,
eqtt_to_assert,
band_wf,
assert-qeq,
bfalse_wf,
equal_wf,
iff_transitivity,
iff_weakening_uiff,
assert_of_bor,
assert_of_band,
eqff_to_assert,
bool_cases_sqequal,
assert-bnot,
sum_wf,
istype-int,
istype-nat,
rat-interval-dimension_wf,
assert-inhabited-rat-cube,
qle_wf,
qmul_preserves_qle,
qdiv_wf,
qadd_wf,
qmul_wf,
int-subtype-rationals,
qmul-qdiv-cancel,
q_le_wf,
assert-q_le-eq,
qadd_preserves_qle,
qadd_ac_1_q,
qadd_inv_assoc_q,
q_distrib,
qmul_one_qrng,
qadd_comm_q,
qinverse_q,
mon_ident_q
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
lambdaFormation_alt,
setElimination,
thin,
rename,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesisEquality,
hypothesis,
productElimination,
independent_isectElimination,
instantiate,
cumulativity,
sqequalRule,
independent_pairFormation,
natural_numberEquality,
inhabitedIsType,
dependent_functionElimination,
because_Cache,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
lambdaEquality_alt,
axiomEquality,
functionIsTypeImplies,
isect_memberEquality_alt,
isectIsTypeImplies,
setIsType,
applyEquality,
equalityIstype,
universeIsType,
unionElimination,
imageElimination,
universeEquality,
imageMemberEquality,
baseClosed,
promote_hyp,
intEquality,
unionEquality,
productEquality,
productIsType,
unionIsType,
inlFormation_alt,
inrFormation_alt,
equalityElimination,
dependent_pairFormation_alt,
voidElimination,
functionIsType,
sqequalBase,
minusEquality
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[c:\{c:\mBbbQ{}Cube(k)| \muparrow{}Inhabited(c)\} ]. \mforall{}[h:\mBbbQ{}Cube(k)].
((\muparrow{}is-half-cube(k;h;c)) {}\mRightarrow{} (dim(h) = dim(c)))
Date html generated:
2020_05_20-AM-09_19_49
Last ObjectModification:
2019_11_02-PM-07_36_37
Theory : rationals
Home
Index