Commit 2023-02-06 07:13 0716ef58

View on Github →

feat: port Combinatorics.SetFamily.Kleitman (#2071)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/Kleitman.lean

added theorem Finset.card_bunionᵢ_le_of_intersecting