Commit 2023-02-04 13:28 b3d0c43f

View on Github →

feat: port Order.Partition.Finpartition (#1765)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Basic.lean

Created Mathlib/Order/Partition/Finpartition.lean

added def Finpartition.IsAtom.uniqueFinpartition

added def Finpartition.atomise

added theorem Finpartition.atomise_empty

added def Finpartition.avoid

added def Finpartition.bind

added theorem Finpartition.bunionᵢ_filter_atomise

added theorem Finpartition.bunionᵢ_parts

added theorem Finpartition.card_atomise_le

added theorem Finpartition.card_bind

added theorem Finpartition.card_bot

added theorem Finpartition.card_extend

added theorem Finpartition.card_filter_atomise_le_two_pow

added theorem Finpartition.card_mono

added theorem Finpartition.card_parts_le_card

added def Finpartition.copy

added theorem Finpartition.default_eq_empty

added theorem Finpartition.exists_le_of_le

added theorem Finpartition.exists_mem

added def Finpartition.extend

added def Finpartition.indiscrete

added theorem Finpartition.mem_atomise

added theorem Finpartition.mem_avoid

added theorem Finpartition.mem_bind

added theorem Finpartition.mem_bot_iff

added theorem Finpartition.ne_bot

added theorem Finpartition.nonempty_of_mem_parts

added def Finpartition.ofErase

added def Finpartition.ofSubset

added theorem Finpartition.parts_bot

added theorem Finpartition.parts_eq_empty_iff

added theorem Finpartition.parts_inf

added theorem Finpartition.parts_nonempty

added theorem Finpartition.parts_nonempty_iff

added theorem Finpartition.parts_top_subset

added theorem Finpartition.parts_top_subsingleton

added theorem Finpartition.sum_card_parts

added structure Finpartition