Number_of_Elements_in_Partition
Provedcombinatoricsproofwiki
Let be a set. Let there be a partition on of subsets, each of which has elements. Then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Number_of_Elements_in_Partition (S : Finset ℕ) (n m : ℕ) (B : Fin n → Finset ℕ) (hpart : ∀ x, x ∈ S ↔ ∃ i, x ∈ B i) (hsize : ∀ i, (B i).card = m) (hdisj : ∀ i j, i ≠ j → Disjoint (B i) (B j)) : S.card = n * m := by sorry
Source