---

Step * of Lemma groupoid-nerve-filler_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-filler(G;I;J;x;i;box) ∈ cubical-nerve(cat(G))(I))
BY
{ ProveWfLemma }

---

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-filler(G;I;J;x;i;box)  \mmember{}  cubical-nerve(cat(G))(I))


By

---

Latex:
ProveWfLemma

---

Home Index