---

Step * of Lemma lattice-fset-meet_functionality_wrt_subset

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

---

Latex:

---

Latex:
\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:
(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