---

Step * 1 1 of Lemma dM-hom-basis


1. I : fset(ℕ)
2. l : BoundedLattice
3. h : Hom(dM(I);l)
⊢ h ∈ Hom(free-DeMorgan-lattice(names(I);NamesDeq);l)
BY
{ InferEqualType }

1
1. I : fset(ℕ)
2. l : BoundedLattice
3. h : Hom(dM(I);l)
⊢ Hom(dM(I);l) = Hom(free-DeMorgan-lattice(names(I);NamesDeq);l) ∈ Type

2
1. I : fset(ℕ)
2. l : BoundedLattice
3. h : Hom(dM(I);l)
4. Hom(dM(I);l) = Hom(free-DeMorgan-lattice(names(I);NamesDeq);l) ∈ Type
⊢ h ∈ Hom(dM(I);l)

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  l  :  BoundedLattice
3.  h  :  Hom(dM(I);l)
\mvdash{}  h  \mmember{}  Hom(free-DeMorgan-lattice(names(I);NamesDeq);l)


By

---

Latex:
InferEqualType

---

Home Index