---

Step * of Lemma lattice-fset-join_functionality_wrt_subset

No Annotations
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  \/(s1) ≤ \/(s2) supposing s1 ⊆ s2
BY
{ TACTIC:(Auto THEN (InstLemma `lattice-fset-join-is-lub` [⌜l⌝;⌜eq⌝]⋅ THENA Auto) THEN D -1 THEN BHyp -1 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[l:BoundedLattice].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[s1,s2:fset(Point(l))].
    \mbackslash{}/(s1)  \mleq{}  \mbackslash{}/(s2)  supposing  s1  \msubseteq{}  s2


By

---

Latex:
TACTIC:(Auto
                THEN  (InstLemma  `lattice-fset-join-is-lub`  [\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  BHyp  -1
                THEN  Auto)

---

Home Index