### Nuprl Lemma : face-name_wf

`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f:I-face(X;I)].  (face-name(f) ∈ nameset(I) × ℕ2)`

Proof

Definitions occuring in Statement :  face-name: `face-name(f)` I-face: `I-face(X;I)` cubical-set: `CubicalSet` nameset: `nameset(L)` coordinate_name: `Cname` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` member: `t ∈ T` product: `x:A × B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` face-name: `face-name(f)` I-face: `I-face(X;I)` pi1: `fst(t)` pi2: `snd(t)`
Lemmas referenced :  I-face_wf list_wf coordinate_name_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule independent_pairEquality sqequalHypSubstitution productElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination isect_memberEquality because_Cache

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I:Cname  List].  \mforall{}[f:I-face(X;I)].    (face-name(f)  \mmember{}  nameset(I)  \mtimes{}  \mBbbN{}2)

Date html generated: 2016_06_16-PM-05_49_15
Last ObjectModification: 2015_12_28-PM-04_31_15

Theory : cubical!sets

Home Index