---

Step * of Lemma nc-e'-p

∀[I,J:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[z:Point(dM(I))]. ∀[i:ℕ]. ∀[j:{j:ℕ| ¬j ∈ J} ].
  ((i/z) ⋅ f = f,i=j ⋅ (j/dM-lift(J;I;f) z) ∈ J ⟶ I+i)
BY
{ (Auto
   THEN (RWO "nh-comp-sq" 0 THENA Auto)
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN RepUR ``compose`` 0) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
4. z : Point(dM(I))
5. i : ℕ
6. j : {j:ℕ| ¬j ∈ J} 
7. x : names(I+i)
⊢ (dM-lift(J;I;f) ((i/z) x)) = (dM-lift(J;J+j;(j/dM-lift(J;I;f) z)) (f,i=j x)) ∈ Point(dM(J))

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[z:Point(dM(I))].  \mforall{}[i:\mBbbN{}].  \mforall{}[j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  ].
    ((i/z)  \mcdot{}  f  =  f,i=j  \mcdot{}  (j/dM-lift(J;I;f)  z))


By

---

Latex:
(Auto
  THEN  (RWO  "nh-comp-sq"  0  THENA  Auto)
  THEN  Unfold  `names-hom`  0
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``compose``  0)

---

Home Index