Commit 2026-08-10 07:28 985d9701

View on Github →

chore(Order/Filter/IsBounded): use to_dual (#37751) use to_dual for Filter.IsBounded

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

Modified Mathlib/Order/Filter/IsBounded.lean

deleted theorem Antitone.frequently_ge_map_of_frequently_le

deleted theorem Antitone.isBoundedUnder_ge_comp

deleted theorem Antitone.isBoundedUnder_ge_comp_iff

deleted theorem Antitone.isCoboundedUnder_ge_of_isCobounded

deleted theorem BddBelow.isBoundedUnder

deleted theorem BddBelow.isBoundedUnder_of_range

deleted theorem Filter.IsBounded.isCobounded_ge

modified theorem Filter.IsBounded.isCobounded_le

deleted theorem Filter.IsBoundedUnder.bddBelow_range

deleted theorem Filter.IsBoundedUnder.bddBelow_range_of_cofinite

deleted theorem Filter.IsBoundedUnder.eventually_ge

deleted theorem Filter.IsBoundedUnder.ge_of_finite

deleted theorem Filter.IsBoundedUnder.inf

deleted theorem Filter.IsBoundedUnder.isCoboundedUnder_ge

deleted theorem Filter.IsBoundedUnder.mono_ge

deleted theorem Filter.IsCobounded.frequently_le

deleted theorem Filter.IsCobounded.of_frequently_le

deleted theorem Filter.IsCoboundedUnder.frequently_le

deleted theorem Filter.IsCoboundedUnder.of_frequently_le

deleted theorem Filter.Tendsto.isBoundedUnder_ge_atTop

deleted theorem Filter.isBoundedUnder_ge_add

deleted theorem Filter.isBoundedUnder_ge_inf

deleted theorem Filter.isBoundedUnder_ge_sum

deleted theorem Filter.isBoundedUnder_iff_eventually_bddBelow

deleted theorem Filter.isBoundedUnder_of_eventually_ge

deleted theorem Filter.isBounded_ge_atTop

deleted theorem Filter.isBounded_ge_of_bot

deleted theorem Filter.isCoboundedUnder_ge_add

deleted theorem Filter.isCoboundedUnder_ge_of_eventually_le

deleted theorem Filter.isCoboundedUnder_ge_of_le

modified theorem Filter.isCoboundedUnder_le_add

deleted theorem Filter.isCobounded_ge_of_top

deleted theorem Filter.not_isBoundedUnder_of_tendsto_atBot

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

deleted theorem OrderIso.isBoundedUnder_ge_comp

deleted theorem isBoundedUnder_ge_finset_inf'

deleted theorem isBoundedUnder_ge_finset_inf

deleted theorem isCoboundedUnder_ge_finset_inf'