---

Step * of Lemma lattice-fset-join-union

∀[l:BoundedLattice]. ∀[eq:EqDecider(Point(l))]. ∀[s1,s2:fset(Point(l))].  (\/(s1 ⋃ s2) = \/(s1) ∨ \/(s2) ∈ Point(l))
BY
{ (Intros THEN RepeatFor 2 (MoveToConcl (-1)) THEN UsingVars [`eq'] (BLemma `fset-induction` THEN Auto)⋅) }

1
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. s2 : fset(Point(l))
⊢ \/({} ⋃ s2) = \/({}) ∨ \/(s2) ∈ Point(l)

2
1. l : BoundedLattice
2. eq : EqDecider(Point(l))
3. s1 : fset(Point(l))
4. x : Point(l)
5. ∀s2:fset(Point(l)). (\/(s1 ⋃ s2) = \/(s1) ∨ \/(s2) ∈ Point(l))
6. ¬x ∈ s1
7. s2 : fset(Point(l))
⊢ \/(fset-add(eq;x;s1) ⋃ s2) = \/(fset-add(eq;x;s1)) ∨ \/(s2) ∈ Point(l)

---

Latex:

---

Latex:
\mforall{}[l:BoundedLattice].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[s1,s2:fset(Point(l))].
    (\mbackslash{}/(s1  \mcup{}  s2)  =  \mbackslash{}/(s1)  \mvee{}  \mbackslash{}/(s2))


By

---

Latex:
(Intros
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  UsingVars  [`eq']  (BLemma  `fset-induction`  THEN  Auto)\mcdot{})

---

Home Index