---

Step * of Lemma groupoid-nerve-filler0_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-filler0(I;x;box) ∈ cubical-nerve(cat(G))(I) supposing ↑null(J)
BY
{ (Auto THEN DVar `J' THEN Reduce (-1) THEN Auto THEN Thin (-1)) }

1
1. G : Groupoid
2. I : Cname List
3. x : nameset(I)
4. i : ℕ2
5. box : open_box(cubical-nerve(cat(G));I;[];x;i)
⊢ groupoid-nerve-filler0(I;x;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-filler0(I;x;box)  \mmember{}  cubical-nerve(cat(G))(I)  supposing  \muparrow{}null(J)


By

---

Latex:
(Auto  THEN  DVar  `J'  THEN  Reduce  (-1)  THEN  Auto  THEN  Thin  (-1))

---

Home Index