Commit 2025-03-19 10:04 49bf7285

chore(Order): split long file CompleteLattice.lean (#23064) This PR splits the long file Mathlib.Order.CompleteLattice into three files:

• CompleteLattice.Defs: definition of CompleteSemilattice{Inf,Sup} and CompleteLattice, important constructors
• CompleteLattice.Basic: basic theory (in particular the declarations that GaloisConnection.Basic depends on)
• CompleteLattice.Lemmas: results that need more imports (such as sups on Nat or Bool) This file appears on the long pole between Order.Hom.Set and Order.GaloisConnection.Basic. The PR probably won't improve that metric much since the next import, Mathlib.Order.CompleteBooleanAlgebra still imports Mathlib.Order.CompleteLattice.Lemmas (and the differences between those files are small anyway).