---

Step * 1 of Lemma face-image_wf


1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : nameset(I)
6. f2 : ℕ2
7. f3 : X(I-[x])
8. ↑isname(f x)
⊢ <f x, f2, f(f3)> ∈ x:nameset(K) × ℕ2 × X(K-[x])
BY
{ (DVar `x'
   THEN (FLemma `assert-isname` [-1] THENA Auto)
   THEN (Assert ⌜f ∈ name-morph(I-[x];K-[f x])⌝⋅ THENM Auto)
   THEN BLemma `name-morph_subtype_remove1` ⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  I  :  Cname  List
3.  K  :  Cname  List
4.  f  :  name-morph(I;K)
5.  x  :  nameset(I)
6.  f2  :  \mBbbN{}2
7.  f3  :  X(I-[x])
8.  \muparrow{}isname(f  x)
\mvdash{}  <f  x,  f2,  f(f3)>  \mmember{}  x:nameset(K)  \mtimes{}  \mBbbN{}2  \mtimes{}  X(K-[x])


By

---

Latex:
(DVar  `x'
  THEN  (FLemma  `assert-isname`  [-1]  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}f  \mmember{}  name-morph(I-[x];K-[f  x])\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  BLemma  `name-morph\_subtype\_remove1`  \mcdot{}
  THEN  Auto)

---

Home Index