---

Step * of Lemma fset-size-union

∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[a,b:fset(T)].  (||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ) supposing valueall-type(T)
BY
{ (Auto THEN RepeatFor 2 (MoveToConcl (-1)⋅) THEN (UsingVars [`eq'] (BLemma `fset-induction`)  THEN Auto)⋅) }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : fset(T)
⊢ ||{} ⋃ b|| = ((||{}|| + ||b||) - ||{} ⋂ b||) ∈ ℤ

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. a : fset(T)
5. x : T
6. ∀b:fset(T). (||a ⋃ b|| = ((||a|| + ||b||) - ||a ⋂ b||) ∈ ℤ)
7. ¬x ∈ a
8. b : fset(T)
⊢ ||fset-add(eq;x;a) ⋃ b|| = ((||fset-add(eq;x;a)|| + ||b||) - ||fset-add(eq;x;a) ⋂ b||) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b:fset(T)].    (||a  \mcup{}  b||  =  ((||a||  +  ||b||)  -  ||a  \mcap{}  b||)) 
    supposing  valueall-type(T)


By

---

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

---

Home Index