---

Step * 2 2 of Lemma lattice-fset-join-is-lub


1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. u : Point(l)
4. ∀x:Point(l). (x ∈ {} ⇒ x ≤ u)
⊢ \/({}) ≤ u
BY
{ (RepUR ``lattice-fset-join empty-fset`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  l  :  BoundedLattice
2.  eq  :  EqDecider(Point(l))
3.  u  :  Point(l)
4.  \mforall{}x:Point(l).  (x  \mmember{}  \{\}  {}\mRightarrow{}  x  \mleq{}  u)
\mvdash{}  \mbackslash{}/(\{\})  \mleq{}  u


By

---

Latex:
(RepUR  ``lattice-fset-join  empty-fset``  0  THEN  Auto)

---

Home Index