Commit 2024-07-22 19:50 733640fc

View on Github →

feat(Topology/Algebra/Order/LiminfLimsup): generalize map liminf and map limsup lemmas (#14591) Generalize map liminf and map limsup lemmas. Instead of assuming boundedness in both directions, it suffices to assume boundedness in one direction and coboundedness in the other direction.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Antitone.frequently_ge_map_of_frequently_le

added theorem Antitone.frequently_le_map_of_frequently_ge

added theorem Antitone.isCoboundedUnder_ge_of_isCobounded

added theorem Antitone.isCoboundedUnder_le_of_isCobounded

added theorem Filter.IsCobounded.frequently_ge

added theorem Filter.IsCobounded.frequently_le

added theorem Filter.IsCobounded.of_frequently_ge

added theorem Filter.IsCobounded.of_frequently_le

added theorem Monotone.frequently_ge_map_of_frequently_ge

added theorem Monotone.frequently_le_map_of_frequently_le

added theorem Monotone.isCoboundedUnder_ge_of_isCobounded

added theorem Monotone.isCoboundedUnder_le_of_isCobounded

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

Modified Mathlib/Topology/Instances/ENNReal.lean