Commit 2023-09-13 10:00 33c02ffb

View on Github →

chore: Generalise and move liminf/limsup lemmas (#6846) Forward-ports https://github.com/leanprover-community/mathlib/pull/18628

Estimated changes

Modified Mathlib/Data/Set/Finite.lean

modified theorem Set.infinite_of_not_bddBelow

Modified Mathlib/Order/Bounds/Basic.lean

modified theorem BddAbove.union

modified theorem BddBelow.union

added def ScottContinuous

modified theorem bddAbove_insert

modified theorem bddAbove_union

modified theorem bddBelow_insert

modified theorem bddBelow_union

Modified Mathlib/Order/Directed.lean

deleted def ScottContinuous

Modified Mathlib/Order/LiminfLimsup.lean

modified theorem Filter.IsBoundedUnder.bddAbove_range

modified theorem Filter.IsBoundedUnder.bddAbove_range_of_cofinite

modified theorem Filter.IsBoundedUnder.bddBelow_range

modified theorem Filter.IsBoundedUnder.bddBelow_range_of_cofinite

added theorem Filter.Tendsto.isBoundedUnder_ge_atTop

added theorem Filter.Tendsto.isBoundedUnder_le_atBot

added theorem Filter.bddAbove_range_of_tendsto_atTop_atBot

added theorem Filter.bddBelow_range_of_tendsto_atTop_atTop

added theorem Filter.gt_mem_sets_of_limsInf_gt

added theorem Filter.isBounded_ge_atTop

added theorem Filter.isBounded_le_atBot

added theorem Filter.lt_mem_sets_of_limsSup_lt

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

deleted theorem Filter.Tendsto.isBoundedUnder_ge_atTop

deleted theorem Filter.Tendsto.isBoundedUnder_le_atBot

deleted theorem bddAbove_range_of_tendsto_atTop_atBot

deleted theorem bddBelow_range_of_tendsto_atTop_atTop

deleted theorem gt_mem_sets_of_limsInf_gt

deleted theorem isBounded_ge_atTop

deleted theorem isBounded_le_atBot

deleted theorem lt_mem_sets_of_limsSup_lt