---

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

∀[I,J:fset(ℕ)]. ∀[g:J ⟶ I]. ∀[j,k,v:ℕ].  g,j=v ⋅ e(v;k) = g,j=k ∈ J+k ⟶ I+j supposing ¬v ∈ J
BY
{ (Auto
   THEN Unfold `names-hom` 0
   THEN (FunExt THENA Auto)
   THEN RepUR ``nh-comp dma-lift-compose`` 0
   THEN Fold `dM` 0
   THEN Fold `dM-lift` 0
   THEN RepUR ``nc-e\'`` 0
   THEN AutoSplit
   THEN (((FLemma `not-added-name` [-1] THENA Auto)
          THEN (GenConclTerm ⌜g x⌝⋅ THENA Auto)
          THEN BLemma `dM-lift-is-id2` 
          THEN Auto)
   ORELSE (RWO "dM-lift-inc" 0 THENA Auto)
   )
   THEN RepUR ``nc-e`` 0
   THEN AutoSplit) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. g : J ⟶ I
4. j : ℕ
5. k : ℕ
6. v : ℕ
7. ¬v ∈ J
8. x : names(I+j)
9. x ≠ j
10. x ∈ names(I)
11. v1 : Point(dM(J))
12. (g x) = v1 ∈ Point(dM(J))
13. i : names(J)
14. i = v ∈ ℤ
⊢ <k> = <i> ∈ Point(dM(J+k))

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[g:J  {}\mrightarrow{}  I].  \mforall{}[j,k,v:\mBbbN{}].    g,j=v  \mcdot{}  e(v;k)  =  g,j=k  supposing  \mneg{}v  \mmember{}  J


By

---

Latex:
(Auto
  THEN  Unfold  `names-hom`  0
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``nh-comp  dma-lift-compose``  0
  THEN  Fold  `dM`  0
  THEN  Fold  `dM-lift`  0
  THEN  RepUR  ``nc-e\mbackslash{}'``  0
  THEN  AutoSplit
  THEN  (((FLemma  `not-added-name`  [-1]  THENA  Auto)
                THEN  (GenConclTerm  \mkleeneopen{}g  x\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  BLemma  `dM-lift-is-id2` 
                THEN  Auto)
  ORELSE  (RWO  "dM-lift-inc"  0  THENA  Auto)
  )
  THEN  RepUR  ``nc-e``  0
  THEN  AutoSplit)

---

Home Index