---

Step * 2 of Lemma nerve_box_label_wf

.....subterm..... T:t
2:n
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(C);I;J;x;i)
7. L : name-morph(I;[])
8. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
9. x1 : nameset(I)@i
10. v2 : ℕ2@i
11. v3 : Functor(poset-cat(I-[x1]);C)@i
12. (<x1, v2, v3> ∈ box) ∧ (direction(<x1, v2, v3>) = (L dimension(<x1, v2, v3>)) ∈ ℕ2)@i
13. nerve-box-face(box;L)
= <x1, v2, v3>
∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)} @i
⊢ L ∈ cat-ob(poset-cat(I-[x1]))
BY
{ (RepUR ``poset-cat cat-ob`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  C  :  SmallCategory
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  box  :  open\_box(cubical-nerve(C);I;J;x;i)
7.  L  :  name-morph(I;[])
8.  ((L  x)  =  i)  \mvee{}  (\mneg{}\muparrow{}null(J))
9.  x1  :  nameset(I)@i
10.  v2  :  \mBbbN{}2@i
11.  v3  :  Functor(poset-cat(I-[x1]);C)@i
12.  (<x1,  v2,  v3>  \mmember{}  box)  \mwedge{}  (direction(<x1,  v2,  v3>)  =  (L  dimension(<x1,  v2,  v3>)))@i
13.  nerve-box-face(box;L)  =  <x1,  v2,  v3>@i
\mvdash{}  L  \mmember{}  cat-ob(poset-cat(I-[x1]))


By

---

Latex:
(RepUR  ``poset-cat  cat-ob``  0  THEN  Auto)

---

Home Index