---

Step * of Lemma dM-dma-hom-invariant

∀[I:fset(ℕ)]. ∀[J:{J:fset(ℕ)| I ⊆ J} ]. ∀[h:dma-hom(dM(J);dM(I))].
  ∀[x:Point(dM(I))]. ((h x) = x ∈ Point(dM(I))) supposing ∀i:names(I). ((h <i>) = <i> ∈ Point(dM(I)))
BY
{ (InstLemma `dM-hom-invariant` [] THEN RepeatFor 5 (ParallelLast') THEN Auto) }

1
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. h : dma-hom(dM(J);dM(I))
4. i : names(I)
5. (h <i>) = <i> ∈ Point(dM(I))
6. (h <i>) = <i> ∈ Point(dM(I))
⊢ (h <1-i>) = <1-i> ∈ Point(dM(I))

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[J:\{J:fset(\mBbbN{})|  I  \msubseteq{}  J\}  ].  \mforall{}[h:dma-hom(dM(J);dM(I))].
    \mforall{}[x:Point(dM(I))].  ((h  x)  =  x)  supposing  \mforall{}i:names(I).  ((h  <i>)  =  <i>)


By

---

Latex:
(InstLemma  `dM-hom-invariant`  []  THEN  RepeatFor  5  (ParallelLast')  THEN  Auto)

---

Home Index