---

Step * of Lemma dM-homs-equal

∀[I:fset(ℕ)]. ∀[l:BoundedLattice].
  ∀eq:EqDecider(Point(l))
    ∀[h1,h2:Hom(dM(I);l)].
      h1 = h2 ∈ (Point(dM(I)) ⟶ Point(l)) 
      supposing ∀i:names(I). (((h1 <i>) = (h2 <i>) ∈ Point(l)) ∧ ((h1 <1-i>) = (h2 <1-i>) ∈ Point(l)))
BY
{ (Auto THEN (FunExt THENA Auto) THEN (InstLemma `dM-hom-basis` [⌜I⌝;⌜x⌝;⌜l⌝;⌜eq⌝]⋅ THENA Auto)) }

1
1. I : fset(ℕ)
2. l : BoundedLattice
3. eq : EqDecider(Point(l))
4. h1 : Hom(dM(I);l)
5. h2 : Hom(dM(I);l)
6. ∀i:names(I). (((h1 <i>) = (h2 <i>) ∈ Point(l)) ∧ ((h1 <1-i>) = (h2 <1-i>) ∈ Point(l)))
7. x : Point(dM(I))
8. ∀[h:Hom(dM(I);l)]. ((h x) = \/(λs./\(λx.(h free-dl-inc(x))"(s))"(x)) ∈ Point(l))
⊢ (h1 x) = (h2 x) ∈ Point(l)

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[l:BoundedLattice].
    \mforall{}eq:EqDecider(Point(l))
        \mforall{}[h1,h2:Hom(dM(I);l)].
            h1  =  h2  supposing  \mforall{}i:names(I).  (((h1  <i>)  =  (h2  <i>))  \mwedge{}  ((h1  ə-i>)  =  (h2  ə-i>)))


By

---

Latex:
(Auto  THEN  (FunExt  THENA  Auto)  THEN  (InstLemma  `dM-hom-basis`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index