### Nuprl Lemma : A-face-name_wf

[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[f:A-face(X;A;I;alpha)].
(A-face-name(f) ∈ nameset(I) × ℕ2)

Proof

Definitions occuring in Statement :  A-face-name: A-face-name(f) A-face: A-face(X;A;I;alpha) cubical-type: {X ⊢ _} I-cube: X(I) cubical-set: CubicalSet nameset: nameset(L) coordinate_name: Cname list: 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 A-face-name: A-face-name(f) A-face: A-face(X;A;I;alpha) pi1: fst(t) pi2: snd(t)
Lemmas referenced :  A-face_wf I-cube_wf list_wf coordinate_name_wf cubical-type_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{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].  \mforall{}[f:A-face(X;A;I;alpha)].
(A-face-name(f)  \mmember{}  nameset(I)  \mtimes{}  \mBbbN{}2)

Date html generated: 2016_06_16-PM-05_49_37
Last ObjectModification: 2015_12_28-PM-04_30_49

Theory : cubical!sets

Home Index