---

Step * of Lemma nc-e'-lemma5

∀[I,J:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[j:{j:ℕ| ¬j ∈ J} ]. ∀[g:J ⟶ I]. ∀[k:{i1:ℕ| ¬i1 ∈ I+i} ]. ∀[l:{i:ℕ| ¬i ∈ J+j} ].
  (s ⋅ g,i=j,k=l = g ⋅ 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
   THEN RepUR ``nc-s`` 0
   THEN Fold `nc-s` 0
   THEN (Assert I ⊆ I+i+k BY
               EAuto 2)
   THEN (Assert J ⊆ J+j+l BY
               EAuto 2)
   THEN (RWO "dM-lift-s dM-lift-inc" 0 THENA Auto)) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. i : {i:ℕ| ¬i ∈ I} 
4. j : {j:ℕ| ¬j ∈ J} 
5. g : J ⟶ I
6. k : {i1:ℕ| ¬i1 ∈ I+i} 
7. l : {i:ℕ| ¬i ∈ J+j} 
8. x : names(I)
9. I ⊆ I+i+k
10. J ⊆ J+j+l
⊢ (g,i=j,k=l x) = (g x) ∈ Point(dM(J+j+l))

---

Latex:

---

Latex:
\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{}[k:\{i1:\mBbbN{}|  \mneg{}i1  \mmember{}  I+i\}  ].
\mforall{}[l:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  J+j\}  ].
    (s  \mcdot{}  g,i=j,k=l  =  g  \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
  THEN  RepUR  ``nc-s``  0
  THEN  Fold  `nc-s`  0
  THEN  (Assert  I  \msubseteq{}  I+i+k  BY
                          EAuto  2)
  THEN  (Assert  J  \msubseteq{}  J+j+l  BY
                          EAuto  2)
  THEN  (RWO  "dM-lift-s  dM-lift-inc"  0  THENA  Auto))

---

Home Index