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