---

Step * 1 of Lemma dM-dma-hom-invariant


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))
BY
{ DVar `h' }

1
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. h : Hom(dM(J);dM(I))
4. ∀[a:Point(dM(J))]. (¬(h a) = (h ¬(a)) ∈ Point(dM(I)))
5. i : names(I)
6. (h <i>) = <i> ∈ Point(dM(I))
7. (h <i>) = <i> ∈ Point(dM(I))
⊢ (h <1-i>) = <1-i> ∈ Point(dM(I))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  \{J:fset(\mBbbN{})|  I  \msubseteq{}  J\} 
3.  h  :  dma-hom(dM(J);dM(I))
4.  i  :  names(I)
5.  (h  <i>)  =  <i>
6.  (h  <i>)  =  <i>
\mvdash{}  (h  ə-i>)  =  ə-i>


By

---

Latex:
DVar  `h'

---

Home Index