---

Step * of Lemma lattice-fset-meet_functionality_wrt_subset

No Annotations
∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  /\(s1) ≤ /\(s2) supposing s2 ⊆ s1
BY
{ TACTIC:(Auto THEN (InstLemma `lattice-fset-meet-is-glb` [⌜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  s2  \msubseteq{}  s1


By

---

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

---

Home Index