Commit 2025-06-19 19:44 447fa971

View on Github →

feat: more API for monotone functions wrt topology (#26113)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

Modified Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

modified theorem Continuous.measurableEmbedding

modified theorem ContinuousOn.measurableEmbedding

modified theorem IsClosed.measurableSet_image_of_continuousOn_injOn

modified theorem Measurable.measurableEmbedding

added theorem MeasurableSet.image_of_antitoneOn

modified theorem MeasurableSet.image_of_continuousOn_injOn

modified theorem MeasurableSet.image_of_measurable_injOn

added theorem MeasurableSet.image_of_monotoneOn

added theorem MeasurableSet.image_of_monotoneOn_of_continuousOn

modified theorem MeasurableSet.isClopenable'

modified theorem MeasurableSet.standardBorel

modified theorem MeasureTheory.borel_eq_borel_of_le

modified theorem MeasureTheory.isClopenable_iff_measurableSet

modified theorem MeasureTheory.measurableSet_exists_tendsto

modified theorem MeasureTheory.measurableSet_range_of_continuous_injective

modified theorem MeasureTheory.measurableSet_tendsto_fun

Modified Mathlib/Order/Interval/Set/OrdConnected.lean

added theorem Set.OrdConnected.preimage_antitoneOn

added theorem Set.OrdConnected.preimage_monotoneOn

Modified Mathlib/Topology/Order/Basic.lean

added theorem countable_image_gt_image_Iio_within

added theorem countable_image_gt_image_Ioi_within

added theorem countable_image_lt_image_Iio_within

added theorem countable_image_lt_image_Ioi_within

Modified Mathlib/Topology/Order/LeftRight.lean

added theorem continuousWithinAt_iff_continuous_left'_right'

added theorem continuousWithinAt_iff_continuous_left_right

added theorem continuousWithinAt_inter_Iio_iff_Iic

added theorem continuousWithinAt_inter_Ioi_iff_Ici

added theorem nhdsGT_sup_nhdsWithin_singleton

added theorem nhdsWithinLE_sup_nhdsWithinGE

added theorem nhdsWithinLE_sup_nhdsWithinGT

added theorem nhdsWithinLT_sup_nhdsWithinGE

added theorem nhdsWithinLT_sup_nhdsWithinGT

deleted theorem nhdsWithin_right_sup_nhds_singleton

Modified Mathlib/Topology/Order/LeftRightLim.lean

deleted theorem Antitone.countable_not_continuousAt

deleted theorem Monotone.countable_not_continuousAt

deleted theorem Monotone.countable_not_continuousWithinAt_Iio

deleted theorem Monotone.countable_not_continuousWithinAt_Ioi

Modified Mathlib/Topology/Order/LeftRightNhds.lean

added theorem countable_setOf_isolated_left_within

added theorem countable_setOf_isolated_right_within

Modified Mathlib/Topology/Order/Monotone.lean

added theorem Antitone.countable_not_continuousAt

added theorem Antitone.countable_setOf_two_preimages

added theorem AntitoneOn.countable_not_continuousWithinAt

added theorem AntitoneOn.countable_setOf_two_preimages

added theorem Monotone.countable_not_continuousAt

added theorem Monotone.countable_setOf_two_preimages

added theorem MonotoneOn.countable_not_continuousWithinAt

added theorem MonotoneOn.countable_not_continuousWithinAt_Iio

added theorem MonotoneOn.countable_not_continuousWithinAt_Ioi

added theorem MonotoneOn.countable_setOf_two_preimages