---

Step * of Lemma groupoid-nerve-filler1_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-filler1(G;I;J;x;i;box) ∈ cubical-nerve(cat(G))(I) supposing (¬↑null(J)) ∧ (||box|| ≤ 3)
BY
{ (Auto THEN (FLemma `length-open_box-le-3` [-1] THENA 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. ¬↑null(J)
8. ||box|| ≤ 3
9. (∀j'∈J.j' = hd(J) ∈ Cname)
⊢ groupoid-nerve-filler1(G;I;J;x;i;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-filler1(G;I;J;x;i;box)  \mmember{}  cubical-nerve(cat(G))(I) 
    supposing  (\mneg{}\muparrow{}null(J))  \mwedge{}  (||box||  \mleq{}  3)


By

---

Latex:
(Auto  THEN  (FLemma  `length-open\_box-le-3`  [-1]  THENA  Auto))

---

Home Index