Nuprl Lemma : rat-complex-boundary-0-dim
∀[k:ℕ]. ∀[K:0-dim-complex]. (∂(K) ~ [])
Proof
Definitions occuring in Statement :
rat-complex-boundary: ∂(K),
rational-cube-complex: n-dim-complex,
nil: [],
nat: ℕ,
uall: ∀[x:A]. B[x],
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
false: False,
not: ¬A,
less_than': less_than'(a;b),
le: A ≤ B,
squash: ↓T,
sq_stable: SqStable(P),
and: P ∧ Q,
implies: P ⇒ Q,
prop: ℙ,
uimplies: b supposing a,
so_apply: x[s],
nat: ℕ,
int_seg: {i..j-},
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
rational-cube-complex: n-dim-complex,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
istype-nat,
istype-le,
istype-void,
rational-cube-complex_wf,
boundary-of-0-dim-is-nil,
sq_stable__equal,
l_member_wf,
int_subtype_base,
istype-int,
lelt_wf,
set_subtype_base,
rat-cube-dimension_wf,
equal-wf-base,
rational-cube_wf,
sq_stable__l_all
Rules used in proof :
isectIsTypeImplies,
isect_memberEquality_alt,
voidElimination,
lambdaFormation_alt,
independent_pairFormation,
dependent_set_memberEquality_alt,
axiomSqEquality,
imageElimination,
imageMemberEquality,
functionIsTypeImplies,
axiomEquality,
dependent_functionElimination,
equalitySymmetry,
equalityTransitivity,
inhabitedIsType,
productElimination,
because_Cache,
independent_functionElimination,
universeIsType,
setIsType,
baseClosed,
independent_isectElimination,
addEquality,
natural_numberEquality,
minusEquality,
applyEquality,
intEquality,
lambdaEquality_alt,
sqequalRule,
hypothesis,
hypothesisEquality,
isectElimination,
extract_by_obid,
rename,
thin,
setElimination,
sqequalHypSubstitution,
cut,
introduction,
isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[k:\mBbbN{}]. \mforall{}[K:0-dim-complex]. (\mpartial{}(K) \msim{} [])
Date html generated:
2019_10_29-AM-07_58_39
Last ObjectModification:
2019_10_22-AM-10_33_48
Theory : rationals
Home
Index