Commit 2025-03-24 15:26 6995c4c3

View on Github →

chore: split Order.LiminfLimsup (#23250) About a third of Order.LiminfLimsup does not deal with (b)lim(inf|sup) at all, but rather with Is(Co)Bounded(Under). Move these lemmas to the new file Order.Filter.IsBounded.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Field/Instances.lean

Created Mathlib/Order/Filter/IsBounded.lean

added theorem Antitone.frequently_ge_map_of_frequently_le

added theorem Antitone.frequently_le_map_of_frequently_ge

added theorem Antitone.isBoundedUnder_ge_comp

added theorem Antitone.isBoundedUnder_ge_comp_iff

added theorem Antitone.isBoundedUnder_le_comp

added theorem Antitone.isBoundedUnder_le_comp_iff

added theorem Antitone.isCoboundedUnder_ge_of_isCobounded

added theorem Antitone.isCoboundedUnder_le_of_isCobounded

added theorem BddAbove.isBoundedUnder

added theorem BddAbove.isBoundedUnder_of_range

added theorem BddBelow.isBoundedUnder

added theorem BddBelow.isBoundedUnder_of_range

added theorem Filter.IsBounded.isBoundedUnder

added theorem Filter.IsBounded.isCobounded_flip

added theorem Filter.IsBounded.isCobounded_ge

added theorem Filter.IsBounded.isCobounded_le

added theorem Filter.IsBounded.mono

added theorem Filter.IsBoundedUnder.bddAbove_range

added theorem Filter.IsBoundedUnder.bddAbove_range_of_cofinite

added theorem Filter.IsBoundedUnder.bddBelow_range

added theorem Filter.IsBoundedUnder.bddBelow_range_of_cofinite

added theorem Filter.IsBoundedUnder.comp

added theorem Filter.IsBoundedUnder.eventually_ge

added theorem Filter.IsBoundedUnder.eventually_le

added theorem Filter.IsBoundedUnder.ge_of_finite

added theorem Filter.IsBoundedUnder.inf

added theorem Filter.IsBoundedUnder.isCoboundedUnder_flip

added theorem Filter.IsBoundedUnder.isCoboundedUnder_ge

added theorem Filter.IsBoundedUnder.isCoboundedUnder_le

added theorem Filter.IsBoundedUnder.le_of_finite

added theorem Filter.IsBoundedUnder.mono

added theorem Filter.IsBoundedUnder.mono_ge

added theorem Filter.IsBoundedUnder.mono_le

added theorem Filter.IsBoundedUnder.sup

added theorem Filter.IsCobounded.frequently_ge

added theorem Filter.IsCobounded.frequently_le

added theorem Filter.IsCobounded.mk

added theorem Filter.IsCobounded.mono

added theorem Filter.IsCobounded.of_frequently_ge

added theorem Filter.IsCobounded.of_frequently_le

added theorem Filter.IsCoboundedUnder.frequently_ge

added theorem Filter.IsCoboundedUnder.frequently_le

added theorem Filter.IsCoboundedUnder.of_frequently_ge

added theorem Filter.IsCoboundedUnder.of_frequently_le

added theorem Filter.Tendsto.isBoundedUnder_comp

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.isBoundedUnder_const

added theorem Filter.isBoundedUnder_ge_add

added theorem Filter.isBoundedUnder_ge_inf

added theorem Filter.isBoundedUnder_ge_inv

added theorem Filter.isBoundedUnder_ge_sum

added theorem Filter.isBoundedUnder_iff_eventually_bddAbove

added theorem Filter.isBoundedUnder_iff_eventually_bddBelow

added theorem Filter.isBoundedUnder_le_abs

added theorem Filter.isBoundedUnder_le_add

added theorem Filter.isBoundedUnder_le_inv

added theorem Filter.isBoundedUnder_le_mul_of_nonneg

added theorem Filter.isBoundedUnder_le_sum

added theorem Filter.isBoundedUnder_le_sup

added theorem Filter.isBoundedUnder_map_iff

added theorem Filter.isBoundedUnder_of

added theorem Filter.isBoundedUnder_of_eventually_ge

added theorem Filter.isBoundedUnder_of_eventually_le

added theorem Filter.isBoundedUnder_sum

added theorem Filter.isBounded_bot

added theorem Filter.isBounded_ge_atTop

added theorem Filter.isBounded_ge_of_bot

added theorem Filter.isBounded_iff

added theorem Filter.isBounded_le_atBot

added theorem Filter.isBounded_le_of_top

added theorem Filter.isBounded_principal

added theorem Filter.isBounded_sup

added theorem Filter.isBounded_top

added theorem Filter.isCoboundedUnder_ge_add

added theorem Filter.isCoboundedUnder_ge_mul_of_nonneg

added theorem Filter.isCoboundedUnder_ge_of_eventually_le

added theorem Filter.isCoboundedUnder_ge_of_le

added theorem Filter.isCoboundedUnder_le_add

added theorem Filter.isCoboundedUnder_le_of_eventually_le

added theorem Filter.isCoboundedUnder_le_of_le

added theorem Filter.isCobounded_bot

added theorem Filter.isCobounded_ge_of_top

added theorem Filter.isCobounded_le_of_bot

added theorem Filter.isCobounded_principal

added theorem Filter.isCobounded_top

added theorem Filter.not_isBoundedUnder_of_tendsto_atBot

added theorem Filter.not_isBoundedUnder_of_tendsto_atTop

added theorem Monotone.frequently_ge_map_of_frequently_ge

added theorem Monotone.frequently_le_map_of_frequently_le

added theorem Monotone.isBoundedUnder_ge_comp

added theorem Monotone.isBoundedUnder_ge_comp_iff

added theorem Monotone.isBoundedUnder_le_comp

added theorem Monotone.isBoundedUnder_le_comp_iff

added theorem Monotone.isCoboundedUnder_ge_of_isCobounded

added theorem Monotone.isCoboundedUnder_le_of_isCobounded

added theorem OrderIso.isBoundedUnder_ge_comp

added theorem OrderIso.isBoundedUnder_le_comp

added theorem isBoundedUnder_ge_finset_inf'

added theorem isBoundedUnder_ge_finset_inf

added theorem isBoundedUnder_le_finset_sup'

added theorem isBoundedUnder_le_finset_sup

added theorem isCoboundedUnder_ge_finset_inf'

added theorem isCoboundedUnder_le_finset_sup'

added theorem isCoboundedUnder_le_max

Modified Mathlib/Order/LiminfLimsup.lean

deleted theorem Antitone.frequently_ge_map_of_frequently_le

deleted theorem Antitone.frequently_le_map_of_frequently_ge

deleted theorem Antitone.isBoundedUnder_ge_comp

deleted theorem Antitone.isBoundedUnder_ge_comp_iff

deleted theorem Antitone.isBoundedUnder_le_comp

deleted theorem Antitone.isBoundedUnder_le_comp_iff

deleted theorem Antitone.isCoboundedUnder_ge_of_isCobounded

deleted theorem Antitone.isCoboundedUnder_le_of_isCobounded

deleted theorem BddAbove.isBoundedUnder

deleted theorem BddAbove.isBoundedUnder_of_range

deleted theorem BddBelow.isBoundedUnder

deleted theorem BddBelow.isBoundedUnder_of_range

deleted theorem Filter.IsBounded.isBoundedUnder

deleted theorem Filter.IsBounded.isCobounded_flip

deleted theorem Filter.IsBounded.isCobounded_ge

deleted theorem Filter.IsBounded.isCobounded_le

deleted theorem Filter.IsBounded.mono

deleted theorem Filter.IsBoundedUnder.bddAbove_range

deleted theorem Filter.IsBoundedUnder.bddAbove_range_of_cofinite

deleted theorem Filter.IsBoundedUnder.bddBelow_range

deleted theorem Filter.IsBoundedUnder.bddBelow_range_of_cofinite

deleted theorem Filter.IsBoundedUnder.comp

deleted theorem Filter.IsBoundedUnder.eventually_ge

deleted theorem Filter.IsBoundedUnder.eventually_le

deleted theorem Filter.IsBoundedUnder.ge_of_finite

deleted theorem Filter.IsBoundedUnder.inf

deleted theorem Filter.IsBoundedUnder.isCoboundedUnder_flip

deleted theorem Filter.IsBoundedUnder.isCoboundedUnder_ge

deleted theorem Filter.IsBoundedUnder.isCoboundedUnder_le

deleted theorem Filter.IsBoundedUnder.le_of_finite

deleted theorem Filter.IsBoundedUnder.mono

deleted theorem Filter.IsBoundedUnder.mono_ge

deleted theorem Filter.IsBoundedUnder.mono_le

deleted theorem Filter.IsBoundedUnder.sup

deleted theorem Filter.IsCobounded.frequently_ge

deleted theorem Filter.IsCobounded.frequently_le

deleted theorem Filter.IsCobounded.mk

deleted theorem Filter.IsCobounded.mono

deleted theorem Filter.IsCobounded.of_frequently_ge

deleted theorem Filter.IsCobounded.of_frequently_le

deleted theorem Filter.IsCoboundedUnder.frequently_ge

deleted theorem Filter.IsCoboundedUnder.frequently_le

deleted theorem Filter.IsCoboundedUnder.of_frequently_ge

deleted theorem Filter.IsCoboundedUnder.of_frequently_le

deleted theorem Filter.Tendsto.isBoundedUnder_comp

deleted theorem Filter.Tendsto.isBoundedUnder_ge_atTop

deleted theorem Filter.Tendsto.isBoundedUnder_le_atBot

deleted theorem Filter.bddAbove_range_of_tendsto_atTop_atBot

deleted theorem Filter.bddBelow_range_of_tendsto_atTop_atTop

deleted theorem Filter.isBoundedUnder_const

deleted theorem Filter.isBoundedUnder_ge_add

deleted theorem Filter.isBoundedUnder_ge_inf

deleted theorem Filter.isBoundedUnder_ge_inv

deleted theorem Filter.isBoundedUnder_ge_sum

deleted theorem Filter.isBoundedUnder_iff_eventually_bddAbove

deleted theorem Filter.isBoundedUnder_iff_eventually_bddBelow

deleted theorem Filter.isBoundedUnder_le_abs

deleted theorem Filter.isBoundedUnder_le_add

deleted theorem Filter.isBoundedUnder_le_inv

deleted theorem Filter.isBoundedUnder_le_mul_of_nonneg

deleted theorem Filter.isBoundedUnder_le_sum

deleted theorem Filter.isBoundedUnder_le_sup

deleted theorem Filter.isBoundedUnder_map_iff

deleted theorem Filter.isBoundedUnder_of

deleted theorem Filter.isBoundedUnder_of_eventually_ge

deleted theorem Filter.isBoundedUnder_of_eventually_le

deleted theorem Filter.isBoundedUnder_sum

deleted theorem Filter.isBounded_bot

deleted theorem Filter.isBounded_ge_atTop

deleted theorem Filter.isBounded_ge_of_bot

deleted theorem Filter.isBounded_iff

deleted theorem Filter.isBounded_le_atBot

deleted theorem Filter.isBounded_le_of_top

deleted theorem Filter.isBounded_principal

deleted theorem Filter.isBounded_sup

deleted theorem Filter.isBounded_top

deleted theorem Filter.isCoboundedUnder_ge_add

deleted theorem Filter.isCoboundedUnder_ge_mul_of_nonneg

deleted theorem Filter.isCoboundedUnder_ge_of_eventually_le

deleted theorem Filter.isCoboundedUnder_ge_of_le

deleted theorem Filter.isCoboundedUnder_le_add

deleted theorem Filter.isCoboundedUnder_le_of_eventually_le

deleted theorem Filter.isCoboundedUnder_le_of_le

deleted theorem Filter.isCobounded_bot

deleted theorem Filter.isCobounded_ge_of_top

deleted theorem Filter.isCobounded_le_of_bot

deleted theorem Filter.isCobounded_principal

deleted theorem Filter.isCobounded_top

deleted theorem Filter.not_isBoundedUnder_of_tendsto_atBot

deleted theorem Filter.not_isBoundedUnder_of_tendsto_atTop

deleted theorem Monotone.frequently_ge_map_of_frequently_ge

deleted theorem Monotone.frequently_le_map_of_frequently_le

deleted theorem Monotone.isBoundedUnder_ge_comp

deleted theorem Monotone.isBoundedUnder_ge_comp_iff

deleted theorem Monotone.isBoundedUnder_le_comp

deleted theorem Monotone.isBoundedUnder_le_comp_iff

deleted theorem Monotone.isCoboundedUnder_ge_of_isCobounded

deleted theorem Monotone.isCoboundedUnder_le_of_isCobounded

deleted theorem OrderIso.isBoundedUnder_ge_comp

deleted theorem OrderIso.isBoundedUnder_le_comp

deleted theorem isBoundedUnder_ge_finset_inf'

deleted theorem isBoundedUnder_ge_finset_inf

deleted theorem isBoundedUnder_le_finset_sup'

deleted theorem isBoundedUnder_le_finset_sup

deleted theorem isCoboundedUnder_ge_finset_inf'

deleted theorem isCoboundedUnder_le_finset_sup'

deleted theorem isCoboundedUnder_le_max