---

Step * of Lemma nc-e'-comp-m-2

No Annotations
∀[I,J:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[j:{j:ℕ| ¬j ∈ J} ]. ∀[g:J ⟶ I]. ∀[l:{i:ℕ| ¬i ∈ J+j} ].
  (s ⋅ g,i=j ⋅ m(j;l) = g ⋅ s ⋅ s ∈ J+j+l ⟶ I)
BY
{ (Auto
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN (RWW "nh-comp-sq" 0 THENA Auto)
   THEN RepUR ``compose`` 0) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].  \mforall{}[j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  ].  \mforall{}[g:J  {}\mrightarrow{}  I].  \mforall{}[l:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  J+j\}  ].
    (s  \mcdot{}  g,i=j  \mcdot{}  m(j;l)  =  g  \mcdot{}  s  \mcdot{}  s)


By

---

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

---

Home Index