---

Step * of Lemma groupoid-nerve-filler2_wf

∀[G:Groupoid]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
∀[box:open_box(cubical-nerve(cat(G));I;J;x;i)].
  groupoid-nerve-filler2(cat(G);I;J;box) ∈ cubical-nerve(cat(G))(I) supposing 3 < ||box||
BY
{ (Auto
   THEN (FLemma `length-open_box-ge-3` [-1] THENA Auto)
   THEN (Assert ¬↑null(J) BY
               (DVar `J' THEN All Reduce THEN Auto THEN D -1 THEN All Reduce THEN Auto))) }

1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(cubical-nerve(cat(G));I;J;x;i)
7. 3 < ||box||
8. (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
9. ¬↑null(J)
⊢ groupoid-nerve-filler2(cat(G);I;J;box) ∈ cubical-nerve(cat(G))(I)

---

Latex:

---

Latex:
\mforall{}[G:Groupoid].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
\mforall{}[box:open\_box(cubical-nerve(cat(G));I;J;x;i)].
    groupoid-nerve-filler2(cat(G);I;J;box)  \mmember{}  cubical-nerve(cat(G))(I)  supposing  3  <  ||box||


By

---

Latex:
(Auto
  THEN  (FLemma  `length-open\_box-ge-3`  [-1]  THENA  Auto)
  THEN  (Assert  \mneg{}\muparrow{}null(J)  BY
                          (DVar  `J'  THEN  All  Reduce  THEN  Auto  THEN  D  -1  THEN  All  Reduce  THEN  Auto)))

---

Home Index