---

Step * 2 2 of Lemma lattice-fset-meet-is-glb


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index