Commit 2026-10-05 09:13 acf4c061

View on Github →

feat: tag Function.leftLim with to_dual (#43525)

Estimated changes

Modified Mathlib/Tactic/Translate/ToDual.lean

Modified Mathlib/Topology/EMetricSpace/BoundedVariation.lean

deleted theorem BoundedVariationOn.continuousWithinAt_rightLim

deleted theorem BoundedVariationOn.eVariationOn_Ici_eq_Ioi_add_edist

deleted theorem BoundedVariationOn.rightLim

deleted theorem BoundedVariationOn.tendsto_atBot_limUnder

deleted theorem BoundedVariationOn.tendsto_eVariationOn_Icc_right

deleted theorem BoundedVariationOn.tendsto_eVariationOn_Icc_zero_right

deleted theorem BoundedVariationOn.tendsto_rightLim

deleted theorem eVariationOn.eVariationOn_Ico_eq_Icc_of_continuousWithinAt'

deleted theorem eVariationOn.eVariationOn_Ico_eq_Icc_of_continuousWithinAt

deleted theorem eVariationOn.eVariationOn_inter_Ioi_eq_inter_Ici_of_continuousWithinAt

deleted theorem eVariationOn.eVariationOn_rightLim_le

Modified Mathlib/Topology/Order/DenselyOrdered.lean

deleted theorem Ico_subset_closure_interior

deleted theorem Ioc_mem_nhds_iff

deleted theorem IsMin.of_disjoint_nhds_Iio

deleted theorem closure_Iio'

deleted theorem closure_Iio

deleted theorem frontier_Iic'

deleted theorem frontier_Iic

deleted theorem frontier_Iio'

deleted theorem frontier_Iio

deleted theorem interior_Iic'

deleted theorem interior_Iic

deleted theorem interior_Ioc

deleted theorem isClosed_Ioc_iff

deleted theorem left_nhdsWithin_Ioc_neBot

deleted theorem nhdsLT_neBot_of_exists_lt

deleted theorem nhdsWithin_Iio_neBot'

deleted theorem nhdsWithin_Iio_neBot

deleted theorem nonempty_nhds_inter_Iio

deleted theorem right_nhdsWithin_Ioo_neBot

Modified Mathlib/Topology/Order/LeftRightLim.lean

deleted theorem Antitone.continuousWithinAt_Ioi_iff_rightLim_eq

deleted theorem Antitone.le_rightLim

deleted theorem Antitone.rightLim_le

deleted theorem Antitone.tendsto_rightLim

deleted theorem Antitone.tendsto_rightLim_within

deleted theorem ContinuousWithinAt.rightLim_eq

deleted theorem Monotone.continuousWithinAt_Ioi_iff_rightLim_eq

deleted theorem Monotone.le_rightLim

deleted theorem Monotone.rightLim_eq_sInf

deleted theorem Monotone.rightLim_le

deleted theorem Monotone.tendsto_rightLim

deleted theorem Monotone.tendsto_rightLim_within

deleted theorem continuousWithinAt_rightLim_Ici

deleted theorem mapClusterPt_rightLim

deleted theorem rightLim_eq_of_eq_bot

deleted theorem rightLim_eq_of_isTop

deleted theorem rightLim_eq_of_not_tendsto

deleted theorem rightLim_eq_of_tendsto

deleted theorem rightLim_leftLim

deleted theorem rightLim_rightLim

deleted theorem tendsto_atBot_of_mapClusterPt

deleted theorem tendsto_leftLim_atBot_of_tendsto

deleted theorem tendsto_rightLim_atBot_of_tendsto

deleted theorem tendsto_rightLim_of_tendsto

Modified Mathlib/Topology/Order/LeftRightNhds.lean

deleted theorem TFAE_mem_nhdsLE

deleted theorem TFAE_mem_nhdsLT

deleted theorem countable_setOfPred_isolated_left

deleted theorem countable_setOfPred_isolated_left_within

deleted theorem mem_nhdsLE_iff_exists_Icc_subset

deleted theorem mem_nhdsLE_iff_exists_Ioc_subset'

deleted theorem mem_nhdsLE_iff_exists_Ioc_subset

deleted theorem mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset

deleted theorem mem_nhdsLT_iff_exists_Ico_subset

deleted theorem mem_nhdsLT_iff_exists_Ioo_subset'

deleted theorem mem_nhdsLT_iff_exists_Ioo_subset

deleted theorem mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset

deleted theorem nhdsLE_basis_Icc

deleted theorem nhdsLT_basis

deleted theorem nhdsLT_basis_Ico

deleted theorem nhdsLT_basis_Ico_of_exists_lt

deleted theorem nhdsLT_basis_of_exists_lt

deleted theorem nhdsLT_eq_bot_iff

Modified Mathlib/Topology/Order/Monotone.lean

deleted theorem Monotone.tendsto_nhdsGT

deleted theorem MonotoneOn.tendsto_nhdsGT