Commit 2024-11-11 13:54 79e17d0d

chore(Data/Finset): split Basic.lean into many smaller files (#18610) The purpose of this PR is to turn the unwieldy file Data/Finset/Basic.lean into a collection of smaller files. The splits happen mostly based on the sections of the original Basic.lean files, so the import structure can probably be organized in a nicer way. There are also some results in Basic.lean that can find a nicer home if we organize the imports further. Still, I expect these changes help to clean up the file a lot. The following new files are split off from Basic.lean:

• Mathlib/Data/Finset/Attach.lean: Finset.attach and elementary results
• Mathlib/Data/Finset/Dedup.lean: packages Multiset.dedup as Multiset.toFinset; some adjacent results for mapping between multisets, lists and finsets.
• Mathlib/Data/Finset/Defs.lean: definition of the Finset type and its membership predicates
• Mathlib/Data/Finset/Disjoint.lean: results on Disjoint applied to finsets; definition of disjUnion.
• Mathlib/Data/Finset/Empty.lean: definition of ∅ and the Finset.Nonempty predicate
• Mathlib/Data/Finset/Erase.lean: definition of Finset.erase
• Mathlib/Data/Finset/Filter.lean: definition of Finset.filter and the {x ∈ s | p x} set builder notation
• Mathlib/Data/Finset/Insert.lean: definition of Finset.cons, Finset.erase and the singleton finset {a}
• Mathlib/Data/Finset/Lattice/Basic.lean: definition of union and intersection of finsets, lattice structure.
• Mathlib/Data/Finset/Lattice/Lemmas.lean: results on union and intersection needed for the GeneralizedBooleanAlgebra instance in SDiff.lean
• Mathlib/Data/Finset/Range.lean: definition of Finset.range
• Mathlib/Data/Finset/SDiff.lean: definition of set difference on finsets, GeneralizedBooleanAlgebra instance
• Mathlib/Data/Finset/SymmDiff.lean: basic results on the symmetric difference operator (derived from set difference). The following files have seen major changes:
• Mathlib/Data/Finset/Basic.lean: most of its contents have been removed. Still contains a few lesser-used definitions and an assortment of results that didn't have an obvious home at first sight.
• Mathlib/Data/Finset/Lattice/Fold.lean: renamed from Mathlib/Data/Finset/Lattice.lean