Theorem AntitoneOn.tendsto_nhdsWithin_Ioo_left

Modification history

2024-08-19 18:48
Mathlib/Topology/Order/Monotone.lean
feat (Topology.Order): Generalize `Monotone.tendsto_nhdsWithin_Iio` (#15470) …
Added AntitoneOn.tendsto_nhdsWithin_Ioo_leftView on Github →