Commit 2024-08-19 18:48 387efd0c

View on Github →

feat (Topology.Order): Generalize Monotone.tendsto_nhdsWithin_Iio (#15470) Monotone.tendsto_nhdsWithin_Iio and Monotone.tendsto_nhdsWithin_Ioi assume monotonicity on the whole space, but it is sufficient for the function to be monotone on an interval.

Add MonotoneOn.tendsto_nhdsWithin_Ioo_left, MonotoneOn.tendsto_nhdsWithin_Ioo_right, MonotoneOn.tendsto_nhdsWithin_Iio and MonotoneOn.tendsto_nhdsWithin_Ioi.
Simplify the proof of Monotone.tendsto_nhdsWithin_Iio using MonotoneOn.tendsto_nhdsWithin_Iio.

Estimated changes

Modified Mathlib/Topology/Order/Monotone.lean

added theorem Antitone.tendsto_nhdsWithin_Iio

added theorem Antitone.tendsto_nhdsWithin_Ioi

added theorem AntitoneOn.tendsto_nhdsWithin_Iio

added theorem AntitoneOn.tendsto_nhdsWithin_Ioi

added theorem AntitoneOn.tendsto_nhdsWithin_Ioo_left

added theorem AntitoneOn.tendsto_nhdsWithin_Ioo_right

added theorem MonotoneOn.tendsto_nhdsWithin_Iio

added theorem MonotoneOn.tendsto_nhdsWithin_Ioi

added theorem MonotoneOn.tendsto_nhdsWithin_Ioo_left

added theorem MonotoneOn.tendsto_nhdsWithin_Ioo_right