---

Step * 1 1 1 of Lemma sq_stable_fills-A-open-box


1. [X] : CubicalSet
2. [A] : {X ⊢ _}
3. [I] : Cname List
4. [alpha] : X(I)
5. [J] : Cname List
6. [x] : nameset(I)
7. [i] : ℕ2
8. [cube] : A(alpha)
9. bx : A-open-box(X;A;I;alpha;J;x;i)
10. [%] : l_subset(Cname;J;I)
11. i1 : ℕ||bx||
⊢ SqStable(is-A-face(X;A;I;alpha;cube;bx[i1]))
BY
{ (GenConclTerm ⌜bx[i1]⌝⋅ THENA Auto) }

1
1. [X] : CubicalSet
2. [A] : {X ⊢ _}
3. [I] : Cname List
4. [alpha] : X(I)
5. [J] : Cname List
6. [x] : nameset(I)
7. [i] : ℕ2
8. [cube] : A(alpha)
9. bx : A-open-box(X;A;I;alpha;J;x;i)
10. [%] : l_subset(Cname;J;I)
11. i1 : ℕ||bx||
12. v : A-face(X;A;I;alpha)
13. bx[i1] = v ∈ A-face(X;A;I;alpha)
⊢ SqStable(is-A-face(X;A;I;alpha;cube;v))

---

Latex:

---

Latex:

1.  [X]  :  CubicalSet
2.  [A]  :  \{X  \mvdash{}  \_\}
3.  [I]  :  Cname  List
4.  [alpha]  :  X(I)
5.  [J]  :  Cname  List
6.  [x]  :  nameset(I)
7.  [i]  :  \mBbbN{}2
8.  [cube]  :  A(alpha)
9.  bx  :  A-open-box(X;A;I;alpha;J;x;i)
10.  [\%]  :  l\_subset(Cname;J;I)
11.  i1  :  \mBbbN{}||bx||
\mvdash{}  SqStable(is-A-face(X;A;I;alpha;cube;bx[i1]))


By

---

Latex:
(GenConclTerm  \mkleeneopen{}bx[i1]\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index