Commit 2024-08-30 11:38 a4f11e42

View on Github →

feat(Order): A continuous monotone function f maps sSup s to sSup (f '' s) (#15926) This PR shows several lemmas related to the PR title. Note that we already have several lemmas in this direction, but they have very strong hypotheses (like Monotone f when MonotoneOn f s would do). We also remove several duplicated lemmas and replace them with deprecated aliases.

Estimated changes

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

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/Order/Monotone.lean

modified theorem Antitone.map_ciInf_of_continuousAt

modified theorem Antitone.map_ciSup_of_continuousAt

modified theorem Antitone.map_csInf_of_continuousAt

modified theorem Antitone.map_csSup_of_continuousAt

deleted theorem Antitone.map_iInf_of_continuousAt'

deleted theorem Antitone.map_iSup_of_continuousAt'

deleted theorem Antitone.map_sInf_of_continuousAt'

deleted theorem Antitone.map_sSup_of_continuousAt'

added theorem AntitoneOn.map_csInf_of_continuousWithinAt

added theorem AntitoneOn.map_csSup_of_continuousWithinAt

added theorem AntitoneOn.map_sInf_of_continuousWithinAt

added theorem AntitoneOn.map_sSup_of_continuousWithinAt

modified theorem Monotone.map_ciInf_of_continuousAt

modified theorem Monotone.map_ciSup_of_continuousAt

modified theorem Monotone.map_csInf_of_continuousAt

modified theorem Monotone.map_csSup_of_continuousAt

deleted theorem Monotone.map_iInf_of_continuousAt'

deleted theorem Monotone.map_iSup_of_continuousAt'

deleted theorem Monotone.map_sInf_of_continuousAt'

deleted theorem Monotone.map_sSup_of_continuousAt'

added theorem MonotoneOn.map_csInf_of_continuousWithinAt

added theorem MonotoneOn.map_csSup_of_continuousWithinAt

added theorem MonotoneOn.map_sInf_of_continuousWithinAt

added theorem MonotoneOn.map_sSup_of_continuousWithinAt