---

Step * of Lemma lattice-fset-join-le

∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s:fset(Point(l))]. ∀[x:Point(l)].
  (\/(s) ≤ x ⇐⇒ ∀p:Point(l). (p ∈ s ⇒ p ≤ x))
BY
{ (InstLemma `lattice-fset-join-is-lub` []
   THEN RepeatFor 2 (ParallelLast')
   THEN D -1
   THEN Auto
   THEN InstLemma `lattice-le_transitivity` [⌜l⌝;⌜p⌝;⌜\/(s)⌝;⌜x⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:BoundedLattice].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[s:fset(Point(l))].  \mforall{}[x:Point(l)].
    (\mbackslash{}/(s)  \mleq{}  x  \mLeftarrow{}{}\mRightarrow{}  \mforall{}p:Point(l).  (p  \mmember{}  s  {}\mRightarrow{}  p  \mleq{}  x))


By

---

Latex:
(InstLemma  `lattice-fset-join-is-lub`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  D  -1
  THEN  Auto
  THEN  InstLemma  `lattice-le\_transitivity`  [\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}\mbackslash{}/(s)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index