Commit 2025-03-19 17:55 e64ff0f6

chore(Data/Set): split some chunks off large file Data/Set/Lattice.lean (#23098) This PR tries to split some meaningful chunks off of Mathlib.Data.Set.Lattice:

• The new file Mathlib.Data.Set.BooleanAlgebra contains the CompleteAtomicBooleanAlgebra (Set ɑ) instance (and nothing more)
• The new file Mathlib.Data.Set.Lattice.Image contains results on the interaction between the complete lattice structure and image, preimage, image2, MapsTo, InjOn, ... This leaves Mathlib.Data.Set.Lattice focussed on interactions between the lattice operators themselves, more or less. (Although there is a bit that doesn't really fit with lattice theory and might move to Data.Set.Sigma except it would screw up the import direction...) I first tried designing this split by following the import structure but found nothing useful to guide us there: the lemmas that could be upstreamed or at least moved to another file seem to follow no real pattern. So I went instead by looking at the lemma contents entirely and hoped for lake exe shake to catch some import improvements (we get a few tens of files with a few import reductions, and it happens that one of those, Mathlib.Data.Finset.Lattice.Fold is on the long pole).