Commit 2023-08-08 13:50 2be04ba8

View on Github →

feat: Add ConditionallyCompleteLinearOder versions of Monotone.map_limsSup_of_continuousAt etc. (#6107) Generalize some existing lemmas from CompleteLinearOrders to ConditionallyCompleteLinearOrders, adding the appropriate boundedness assumptions:

Monotone.map_limsSup_of_continuousAt + its 3 order-dual variants
Monotone.map_limsup_of_continuousAt + its 3 order-dual variants
Monotone.map_sSup_of_continuousAt' + its 3 order-dual variants
Monotone.map_iSup_of_continuousAt' + its 3 order-dual variants For the first two to work automatically still on CompleteLinearOrders, the existing macro tactic isBoundedDefault about boundedness of filters is used. For the last two to work automatically still on CompleteLinearOrders, a similar new macro tactic bddDefault about boundedness of sets is included in the PR.

Estimated changes

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Order/Basic.lean

modified theorem Antitone.map_sInf_of_continuousAt'

modified theorem Antitone.map_sSup_of_continuousAt'

modified theorem Monotone.map_sInf_of_continuousAt'

modified theorem Monotone.map_sSup_of_continuousAt'