Step * 1 1 of Lemma dM-hom-basis


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

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

2
1. fset(ℕ)
2. BoundedLattice
3. 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