---

Step * of Lemma nerve-box-common-face_wf2

∀[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 (∃j∈J. ¬(j = z ∈ Cname)) ∨ (((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)) ∧b (direction(f) =z flip(L;z) dimension(f)));box))⌝⋅
   THENM ((InstLemma `hd-wf-not-null` [⌜I-face(cubical-nerve(C);I)⌝;⌜filter(λf.((direction(f) =z L dimension(f))
                                                                               ∧b (direction(f) =z flip(L;z) 
                                                                                                   dimension(f)));box)⌝]
           ⋅
           THENA Auto
           )
          THEN (InstLemma `hd_member` [⌜I-face(cubical-nerve(C);I)⌝;⌜filter(λf.((direction(f) =z L dimension(f))
                                                                               ∧b (direction(f) =z flip(L;z) 
                                                                                                   dimension(f)));box)⌝]
                ⋅
                THENA Auto
                )
          THEN All (Fold `nerve-box-common-face`)
          THEN ((RWO "member_filter" (-1) THEN Reduce (-1)) THENA Auto)
          THEN MemTypeCD
          THEN Auto
          THEN ∀h:hyp. (RW assert_pushdownC h THEN Auto) )
   )
   THEN (BLemma `non_null_filter_iff` THEN Auto)
   THEN RepUR ``so_apply`` 0
   THEN D -1) }

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. z : nameset(I)
17. (∃j∈J. ¬(j = z ∈ Cname))
⊢ (∃x∈box. ↑((direction(x) =z L dimension(x)) ∧b (direction(x) =z flip(L;z) dimension(x))))

2
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. z : nameset(I)
17. ((L x) = i ∈ ℕ2) ∧ (¬↑null(J))
⊢ (∃x∈box. ↑((direction(x) =z L dimension(x)) ∧b (direction(x) =z flip(L;z) 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))].  \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{}j\mmember{}J.  \mneg{}(j  =  z))  \mvee{}  (((L  x)  =  i)  \mwedge{}  (\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))
                                                                \mwedge{}\msubb{}  (direction(f)  =\msubz{}  flip(L;z)  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))  \mwedge{}\msubb{}  (direction(f)  =\msubz{}  flip(L;z)  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))
                                                  \mwedge{}\msubb{}  (direction(f)  =\msubz{}  flip(L;z)  dimension(f)));box)\mkleeneclose{}]\mcdot{}
                            THENA  Auto
                            )
                THEN  All  (Fold  `nerve-box-common-face`)
                THEN  ((RWO  "member\_filter"  (-1)  THEN  Reduce  (-1))  THENA  Auto)
                THEN  MemTypeCD
                THEN  Auto
                THEN  \mforall{}h:hyp.  (RW  assert\_pushdownC  h  THEN  Auto)  )
  )
  THEN  (BLemma  `non\_null\_filter\_iff`  THEN  Auto)
  THEN  RepUR  ``so\_apply``  0
  THEN  D  -1)

---

Home Index