Nuprl Lemma : cubical-interval-ap_wf
∀[I:Cname List]. ∀[u:cubical-interval()(I)]. ∀[L:name-morph(I;[])]. (u(L) ∈ ℕ2)
Proof
Definitions occuring in Statement :
cubical-interval-ap: u(L),
cubical-interval: cubical-interval(),
I-cube: X(I),
name-morph: name-morph(I;J),
coordinate_name: Cname,
nil: [],
list: T List,
int_seg: {i..j-},
uall: ∀[x:A]. B[x],
member: t ∈ T,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
cubical-interval-ap: u(L),
subtype_rel: A ⊆r B,
I-cube: X(I),
functor-ob: functor-ob(F),
pi1: fst(t),
cubical-interval: cubical-interval()
Lemmas referenced :
subtype_rel_self,
name-morph_wf,
nil_wf,
coordinate_name_wf,
int_seg_wf,
I-cube_wf,
cubical-interval_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
applyEquality,
hypothesisEquality,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
functionEquality,
hypothesis,
natural_numberEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
because_Cache
Latex:
\mforall{}[I:Cname List]. \mforall{}[u:cubical-interval()(I)]. \mforall{}[L:name-morph(I;[])]. (u(L) \mmember{} \mBbbN{}2)
Date html generated:
2016_06_16-PM-06_50_06
Last ObjectModification:
2015_12_28-PM-04_23_37
Theory : cubical!sets
Home
Index