---

Step * of Lemma lattice-fset-meet-union

No Annotations
∀[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:
No  Annotations
\mforall{}[l:BoundedLattice].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[s1,s2:fset(Point(l))].
    (/\mbackslash{}(s1  \mcup{}  s2)  =  /\mbackslash{}(s1)  \mwedge{}  /\mbackslash{}(s2))


By

---

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

---

Home Index