Commit 2024-11-16 08:30 9a9cb189

chore(Data/Set): split Finite.lean into Defs, Basic, Lemmas (#18619) Data.Set.Finite had a lot of imports and in turn was imported often. So let's split it up along import lines:

• Data/Finite/Defs.lean now contains the definition of Set.Finite
• Data/Set/Finite/Basic.lean knows only Set.Finite and Finset
• Data/Finite/Prod.lean now contains finiteness results of products of sets
• Data/Fintype/Pi.lean now contains finiteness results of sets of functions
• Data/Set/Finite/Lattice.lean contains finiteness results of lattice operations on sets
• Data/Set/Finite/List.lean contains finiteness results on lists converted to sets
• Data/Set/Finite/Monad.lean also knows about the monad structure on Set
• Data/Set/Finite/Powerset.lean contains finiteness results on powersets
• Data/Set/Finite/Range.lean contains finiteness results on Set.range
• Data/Set/Finite/Lemmas.lean is for lemmas about Set.Finite (and therefore does not contain any Finite instances itself).