---

Step * of Lemma dM-lift-nc-1

No Annotations
∀J:fset(ℕ). ∀j:{i:ℕ| ¬i ∈ J} . ∀v:Point(dM(J)).  ((dM-lift(J;J+j;(j1)) v) = v ∈ Point(dM(J)))
BY
{ (Intros THEN RWO "dM-lift-is-id" 0 THEN Auto THEN RepUR ``nc-1`` 0 THEN AutoSplit) }

1
1. J : fset(ℕ)
2. j : {i:ℕ| ¬i ∈ J} 
3. v : Point(dM(J))
4. i : names(J)
5. i = j ∈ ℤ
⊢ {{}} = <i> ∈ Point(dM(J))

---

Latex:

---

Latex:
No  Annotations
\mforall{}J:fset(\mBbbN{}).  \mforall{}j:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  J\}  .  \mforall{}v:Point(dM(J)).    ((dM-lift(J;J+j;(j1))  v)  =  v)


By

---

Latex:
(Intros  THEN  RWO  "dM-lift-is-id"  0  THEN  Auto  THEN  RepUR  ``nc-1``  0  THEN  AutoSplit)

---

Home Index