Step
*
of Lemma
fdl-hom_wf1
∀[X:Type]. ∀[L:BoundedDistributiveLattice]. ∀[f:X ⟶ Point(L)].  (fdl-hom(L;f) ∈ (X List List) ⟶ Point(L))
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[X:Type].  \mforall{}[L:BoundedDistributiveLattice].  \mforall{}[f:X  {}\mrightarrow{}  Point(L)].
    (fdl-hom(L;f)  \mmember{}  (X  List  List)  {}\mrightarrow{}  Point(L))
By
Latex:
ProveWfLemma
Home
Index