---

Step * of Lemma nerve-box-common-face_wf

∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[L:cat-ob(poset-cat(I))]. ∀[z:nameset(I)].
  nerve-box-common-face(box;L;z) ∈ {f:I-face(cubical-nerve(C);I)| 
                                    (f ∈ box)
                                    ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)
                                    ∧ (direction(f) = (flip(L;z) dimension(f)) ∈ ℕ2)}  
  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname))) ∨ (((L x) = i ∈ ℕ2) ∧ (¬↑null(J)))
BY
{ (RepUR ``cat-ob poset-cat`` 0 THEN Auto) }

1
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. z : nameset(I)
9. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname))) ∨ (((L x) = i ∈ ℕ2) ∧ (¬↑null(J)))
⊢ (∃j∈J. ¬(j = z ∈ Cname)) ∨ (((L x) = i ∈ ℕ2) ∧ (¬↑null(J)))

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
\mforall{}[box:open\_box(cubical-nerve(C);I;J;x;i)].  \mforall{}[L:cat-ob(poset-cat(I))].  \mforall{}[z:nameset(I)].
    nerve-box-common-face(box;L;z)  \mmember{}  \{f:I-face(cubical-nerve(C);I)| 
                                                                        (f  \mmember{}  box)
                                                                        \mwedge{}  (direction(f)  =  (L  dimension(f)))
                                                                        \mwedge{}  (direction(f)  =  (flip(L;z)  dimension(f)))\}   
    supposing  (\mexists{}j1\mmember{}J.  (\mexists{}j2\mmember{}J.  \mneg{}(j1  =  j2)))  \mvee{}  (((L  x)  =  i)  \mwedge{}  (\mneg{}\muparrow{}null(J)))


By

---

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

---

Home Index