---

Step * 1 1 1 1 of Lemma groupoid-nerve-filler-uniform

.....assertion..... 
1. i : ℕ2
2. G : Groupoid
3. I : Cname List
4. x : nameset(I)
5. bx : open_box(cubical-nerve(cat(G));I;[];x;i)
6. K : Cname List
7. f : name-morph(I;K)
8. ∀i:nameset(I). ((i ∈ []) ⇒ (↑isname(f i)))
9. ↑isname(f x)
10. True
11. x1 : nameset(I)
12. u2 : ℕ2
13. u3 : Functor(poset-cat(I-[x]);cat(G))
14. x1 = x ∈ nameset(I)
15. u2 = i ∈ ℕ2
16. f x ∈ nameset(K)
17. iota(x) ∈ name-morph(I-[x];I)
18. iota(f x) ∈ name-morph(K-[f x];K)
⊢ f ∈ name-morph(I-[x];K-[f x])
BY
{ TACTIC:(DVar `x' THEN BLemma `name-morph_subtype_remove1` THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  i  :  \mBbbN{}2
2.  G  :  Groupoid
3.  I  :  Cname  List
4.  x  :  nameset(I)
5.  bx  :  open\_box(cubical-nerve(cat(G));I;[];x;i)
6.  K  :  Cname  List
7.  f  :  name-morph(I;K)
8.  \mforall{}i:nameset(I).  ((i  \mmember{}  [])  {}\mRightarrow{}  (\muparrow{}isname(f  i)))
9.  \muparrow{}isname(f  x)
10.  True
11.  x1  :  nameset(I)
12.  u2  :  \mBbbN{}2
13.  u3  :  Functor(poset-cat(I-[x]);cat(G))
14.  x1  =  x
15.  u2  =  i
16.  f  x  \mmember{}  nameset(K)
17.  iota(x)  \mmember{}  name-morph(I-[x];I)
18.  iota(f  x)  \mmember{}  name-morph(K-[f  x];K)
\mvdash{}  f  \mmember{}  name-morph(I-[x];K-[f  x])


By

---

Latex:
TACTIC:(DVar  `x'  THEN  BLemma  `name-morph\_subtype\_remove1`  THEN  Auto)

---

Home Index