Commit 2026-08-24 10:14 2c99b7bf
View on Github →refactor(Data/Set): split long file Lattice.lean (#43030) Split this > 1500 line file into 4 smaller files:
Mathlib.Data.Set.Lattice.Indexed(655 lines): indexed unions and intersections, monotonicity, complements, proposition indexing, and reindexing.Mathlib.Data.Set.Lattice.Bounded(645 lines): bounded unions and intersections, sUnion/sInter, products, directed unions, and surjective reindexing.Mathlib.Data.Set.Lattice.Disjoint(139 lines): disjoint indexed families and equivalences with dependent sums.Mathlib.Data.Set.Lattice.Order(125 lines): intervals, natural-number tails, and interaction with complete-lattice suprema and infima. I tried to do the usual "deprecation stub in a follow-up PR" trick to get git to associate the pre-split history of the file with one of the post-split files, but it doesn't seem to have worked, probably because none of the post-split files match enough of the pre-split file. So I'm merging the deprecation-stub PR back into this one.