Commit 2026-03-16 10:37 a8fbd155

View on Github →

chore: use IsLUB IsGLB in ConditionallyCompleteLattice (#35774) Also, some docstrings in Order.ConditionallyCompleteLattice.Defs are outdated (they still use Lean3 structure notation). #36671 is an orthogonal PR to fix this.

Estimated changes

Modified Mathlib/Algebra/Tropical/Lattice.lean

Modified Mathlib/Data/Int/ConditionallyCompleteOrder.lean

Modified Mathlib/Data/Nat/Lattice.lean

Modified Mathlib/Data/Real/Archimedean.lean

Modified Mathlib/Order/CompleteLatticeIntervals.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

modified theorem isGLB_csInf

modified theorem isLUB_csSup

Modified Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

Modified Mathlib/Order/Copy.lean