---

Step * of Lemma dM-lift-s

∀[I,J:fset(ℕ)].  ∀[x:Point(dM(I))]. ((dM-lift(J;I;s) x) = x ∈ Point(dM(J))) supposing I ⊆ J
BY
{ (Intros THEN InstLemma `dM-lift-is-id2` [⌜I⌝;⌜I⌝;⌜J⌝;⌜s⌝;⌜x⌝]⋅ THEN Auto) }

1
.....wf..... 
1. I : fset(ℕ)
2. J : fset(ℕ)
3. I ⊆ J
4. x : Point(dM(I))
⊢ I ∈ {J:fset(ℕ)| I ⊆ J} 

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].    \mforall{}[x:Point(dM(I))].  ((dM-lift(J;I;s)  x)  =  x)  supposing  I  \msubseteq{}  J


By

---

Latex:
(Intros  THEN  InstLemma  `dM-lift-is-id2`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index