---

Step * of Lemma lattice-fset-join_functionality_wrt_subset2

∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  \/(s1) ≤ \/(s2) supposing s1 ⊆ {0} ⋃ s2
BY
{ (Auto THEN Using [`b',⌜\/({0} ⋃ s2)⌝] (BLemma `lattice-le_transitivity`)⋅ THEN Auto) }

1
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. s1 : fset(Point(l))
4. s2 : fset(Point(l))
5. s1 ⊆ {0} ⋃ s2
⊢ \/({0} ⋃ s2) ≤ \/(s2)

2
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. s1 : fset(Point(l))
4. s2 : fset(Point(l))
5. s1 ⊆ {0} ⋃ s2
⊢ \/(s1) ≤ \/({0} ⋃ s2)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Using  [`b',\mkleeneopen{}\mbackslash{}/(\{0\}  \mcup{}  s2)\mkleeneclose{}]  (BLemma  `lattice-le\_transitivity`)\mcdot{}  THEN  Auto)

---

Home Index