---

Step * 1 3 of Lemma dM-hom-invariant

.....antecedent..... 
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. h : Hom(dM(J);dM(I))
4. ∀i:names(I). (((h <i>) = <i> ∈ Point(dM(I))) ∧ ((h <1-i>) = <1-i> ∈ Point(dM(I))))
5. x : Point(dM(I))
⊢ ∀x,y:Point(dM(I)).  Dec(x = y ∈ Point(dM(I)))
BY
{ ((BLemma `deq-implies` THEN Auto) THEN UseWitness ⌜free-dml-deq(names(I);NamesDeq)⌝⋅) }

1
1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. h : Hom(dM(J);dM(I))
4. ∀i:names(I). (((h <i>) = <i> ∈ Point(dM(I))) ∧ ((h <1-i>) = <1-i> ∈ Point(dM(I))))
5. x : Point(dM(I))
⊢ free-dml-deq(names(I);NamesDeq) ∈ EqDecider(Point(dM(I)))

---

Latex:

---

Latex:
.....antecedent..... 
1.  I  :  fset(\mBbbN{})
2.  J  :  \{J:fset(\mBbbN{})|  I  \msubseteq{}  J\} 
3.  h  :  Hom(dM(J);dM(I))
4.  \mforall{}i:names(I).  (((h  <i>)  =  <i>)  \mwedge{}  ((h  ə-i>)  =  ə-i>))
5.  x  :  Point(dM(I))
\mvdash{}  \mforall{}x,y:Point(dM(I)).    Dec(x  =  y)


By

---

Latex:
((BLemma  `deq-implies`  THEN  Auto)  THEN  UseWitness  \mkleeneopen{}free-dml-deq(names(I);NamesDeq)\mkleeneclose{}\mcdot{})

---

Home Index