---

Step * of Lemma nerve-box-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))].
  nerve-box-face(box;L) ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)}  
  supposing ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
BY
{ ((RepUR ``cat-ob poset-cat`` 0 THEN Auto)
   THEN DVar `box'
   THEN (Assert ⌜¬↑null(filter(λf.(direction(f) =z L dimension(f));box))⌝⋅
   THENM ((InstLemma `hd-wf-not-null` [⌜I-face(cubical-nerve(C);I)⌝;⌜filter(λf.(direction(f) =z L dimension(f));box)⌝]⋅
           THENA Auto
           )
          THEN (InstLemma `hd_member` [⌜I-face(cubical-nerve(C);I)⌝;⌜filter(λf.(direction(f) =z L dimension(f));box)⌝]⋅
                THENA Auto
                )
          THEN All (Fold `nerve-box-face`)
          THEN ((RWO "member_filter" (-1) THEN Reduce (-1)) THENA Auto)
          THEN MemTypeCD
          THEN Auto)
   )
   THEN (BLemma `non_null_filter_iff` THEN Auto)
   THEN RepUR ``so_apply`` 0) }

1
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(cubical-nerve(C);I) List
7. adjacent-compatible(cubical-nerve(C);I;box)
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2.  (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
⊢ (∃x∈box. ↑(direction(x) =z L dimension(x)))

---

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))].
    nerve-box-face(box;L)  \mmember{}  \{f:I-face(cubical-nerve(C);I)| 
                                                      (f  \mmember{}  box)  \mwedge{}  (direction(f)  =  (L  dimension(f)))\}   
    supposing  ((L  x)  =  i)  \mvee{}  (\mneg{}\muparrow{}null(J))


By

---

Latex:
((RepUR  ``cat-ob  poset-cat``  0  THEN  Auto)
  THEN  DVar  `box'
  THEN  (Assert  \mkleeneopen{}\mneg{}\muparrow{}null(filter(\mlambda{}f.(direction(f)  =\msubz{}  L  dimension(f));box))\mkleeneclose{}\mcdot{}
  THENM  ((InstLemma  `hd-wf-not-null`  [\mkleeneopen{}I-face(cubical-nerve(C);I)\mkleeneclose{};
                  \mkleeneopen{}filter(\mlambda{}f.(direction(f)  =\msubz{}  L  dimension(f));box)\mkleeneclose{}]\mcdot{}
                  THENA  Auto
                  )
                THEN  (InstLemma  `hd\_member`  [\mkleeneopen{}I-face(cubical-nerve(C);I)\mkleeneclose{};
                            \mkleeneopen{}filter(\mlambda{}f.(direction(f)  =\msubz{}  L  dimension(f));box)\mkleeneclose{}]\mcdot{}
                            THENA  Auto
                            )
                THEN  All  (Fold  `nerve-box-face`)
                THEN  ((RWO  "member\_filter"  (-1)  THEN  Reduce  (-1))  THENA  Auto)
                THEN  MemTypeCD
                THEN  Auto)
  )
  THEN  (BLemma  `non\_null\_filter\_iff`  THEN  Auto)
  THEN  RepUR  ``so\_apply``  0)

---

Home Index