Commit 2023-02-08 08:54 b2590afd

View on Github →

feat: port Topology.Algebra.Order.LiminfLimsup (#2161)

Estimated changes

Modified Mathlib.lean

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

added theorem Antitone.map_liminf_of_continuousAt

added theorem Antitone.map_liminfₛ_of_continuousAt

added theorem Antitone.map_limsup_of_continuousAt

added theorem Antitone.map_limsupₛ_of_continuousAt

added theorem Filter.Tendsto.bddAbove_range

added theorem Filter.Tendsto.bddAbove_range_of_cofinite

added theorem Filter.Tendsto.bddBelow_range

added theorem Filter.Tendsto.bddBelow_range_of_cofinite

added theorem Filter.Tendsto.isBoundedUnder_ge

added theorem Filter.Tendsto.isBoundedUnder_ge_atTop

added theorem Filter.Tendsto.isBoundedUnder_le

added theorem Filter.Tendsto.isBoundedUnder_le_atBot

added theorem Filter.Tendsto.isCoboundedUnder_ge

added theorem Filter.Tendsto.isCoboundedUnder_le

added theorem Filter.Tendsto.liminf_eq

added theorem Filter.Tendsto.limsup_eq

added theorem Monotone.map_liminf_of_continuousAt

added theorem Monotone.map_liminfₛ_of_continuousAt

added theorem Monotone.map_limsup_of_continuousAt

added theorem Monotone.map_limsupₛ_of_continuousAt

added theorem bddAbove_range_of_tendsto_atTop_atBot

added theorem bddBelow_range_of_tendsto_atTop_atTop

added theorem gt_mem_sets_of_liminfₛ_gt

added theorem infᵢ_eq_of_forall_le_of_tendsto

added theorem isBounded_ge_atTop

added theorem isBounded_ge_nhds

added theorem isBounded_le_atBot

added theorem isBounded_le_nhds

added theorem isCobounded_ge_nhds

added theorem isCobounded_le_nhds

added theorem le_nhds_of_limsupₛ_eq_liminfₛ

added theorem liminfₛ_eq_of_le_nhds

added theorem liminfₛ_nhds

added theorem limsup_eq_tendsto_sum_indicator_atTop

added theorem limsup_eq_tendsto_sum_indicator_nat_atTop

added theorem limsupₛ_eq_of_le_nhds

added theorem limsupₛ_nhds

added theorem lt_mem_sets_of_limsupₛ_lt

added theorem supᵢ_eq_of_forall_le_of_tendsto

added theorem tendsto_of_le_liminf_of_limsup_le

added theorem tendsto_of_liminf_eq_limsup

added theorem tendsto_of_no_upcrossings

added theorem unionᵢ_Ici_eq_Ioi_of_lt_of_tendsto

added theorem unionᵢ_Iic_eq_Iio_of_lt_of_tendsto