Commit 2026-07-02 15:44 52846449

refactor(Order/OrdContinuous): redefine left and right order continuity to not require preserving ⊥/⊤ (#37682) LeftOrdContinuous currently requires that f ⊥ = ⊥, but this means that many functions that are perhaps intuitively left-continuous (like f x = x + 1 on ℝ≥0) are not. In particular, this change means that functions between conditionally complete lattices are LeftOrdContinuous iff they are monotone and topologically left continuous (see MonotoneOn.map_csSup_of_continuousWithinAt for the reverse direction). If one wants the concept that existed before, one can either accept the f ⊥ = ⊥ hypothesis separately or, if the function is between complete lattices, use the left side of a GaloisConnection (which is equivalent, although I think this is not yet in Mathlib). LeftOrdContinuous.continuousWithinAt_Iic is rewritten to accomodate these changes; the superfluous DenselyOrdered assumption is also removed. Zulip thread