---

Step * 1 of Lemma nc-e'-lemma3


1. I : fset(ℕ)
2. i : ℕ
3. ¬i ∈ I
4. J : fset(ℕ)
5. g : J ⟶ I
6. j : ℕ
7. ¬j ∈ J
8. x : names(I)
⊢ (s ⋅ g,i=j x) = (g ⋅ s x) ∈ Point(dM(J+j))
BY
{ (RepUR ``nh-comp nc-e\' nc-s dma-lift-compose`` 0 THEN Fold `dM` 0 THEN Fold `dM-lift` 0) }

1
1. I : fset(ℕ)
2. i : ℕ
3. ¬i ∈ I
4. J : fset(ℕ)
5. g : J ⟶ I
6. j : ℕ
7. ¬j ∈ J
8. x : names(I)
⊢ (dM-lift(J+j;I+i;λx.if (x =z i) then <j> else g x fi ) <x>) = (dM-lift(J+j;J;λx.<x>) (g x)) ∈ Point(dM(J+j))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
3.  \mneg{}i  \mmember{}  I
4.  J  :  fset(\mBbbN{})
5.  g  :  J  {}\mrightarrow{}  I
6.  j  :  \mBbbN{}
7.  \mneg{}j  \mmember{}  J
8.  x  :  names(I)
\mvdash{}  (s  \mcdot{}  g,i=j  x)  =  (g  \mcdot{}  s  x)


By

---

Latex:
(RepUR  ``nh-comp  nc-e\mbackslash{}'  nc-s  dma-lift-compose``  0  THEN  Fold  `dM`  0  THEN  Fold  `dM-lift`  0)

---

Home Index