---

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


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))
BY
{ ((InstHyp [⌜<i>⌝] 4⋅ THENA Auto) THEN Symmetry THEN NthHypEq  (-1) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  \{J:fset(\mBbbN{})|  I  \msubseteq{}  J\} 
3.  h  :  Hom(dM(J);dM(I))
4.  \mforall{}[a:Point(dM(J))].  (\mneg{}(h  a)  =  (h  \mneg{}(a)))
5.  i  :  names(I)
6.  (h  <i>)  =  <i>
7.  (h  <i>)  =  <i>
\mvdash{}  (h  ə-i>)  =  ə-i>


By

---

Latex:
((InstHyp  [\mkleeneopen{}<i>\mkleeneclose{}]  4\mcdot{}  THENA  Auto)  THEN  Symmetry  THEN  NthHypEq    (-1)  THEN  EqCD  THEN  Auto)

---

Home Index