Prove2Me

Sum_Rule_for_Counting

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

combinatoricscountingproofwiki

If S_1 and S_2 are disjoint finite sets, then |S_1 ∪ S_2| = |S_1| + |S_2|.

Preamble
import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Finset.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Finset.Basic

theorem Sum_Rule_for_Counting {α : Type _} [DecidableEq α] (S T : Finset α) (h : Disjoint S T) : (S ∪ T).card = S.card + T.card := by sorry
Source
https://proofwiki.org/wiki/Sum_Rule_for_Counting

View graph