---

Step * of Lemma get_face-dimension

∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)]. ∀[y:nameset(J)]. ∀[c:ℕ2].
  (dimension(get_face(y;c;box)) ~ y)
BY
{ ((UnivCD THENA Auto) THEN (GenConclTerm ⌜get_face(y;c;box)⌝⋅ THENA Auto)) }

1
1. X : CubicalSet
2. I : Cname List
3. J : Cname List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(X;I;J;x;i)
7. y : nameset(J)
8. c : ℕ2
9. v : {f:I-face(X;I)| (f ∈ box) ∧ (face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))} 
10. get_face(y;c;box) = v ∈ {f:I-face(X;I)| (f ∈ box) ∧ (face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))} 
⊢ dimension(v) ~ y

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,J:Cname  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[box:open\_box(X;I;J;x;i)].
\mforall{}[y:nameset(J)].  \mforall{}[c:\mBbbN{}2].
    (dimension(get\_face(y;c;box))  \msim{}  y)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (GenConclTerm  \mkleeneopen{}get\_face(y;c;box)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index