Theorem AntitoneOn.tendsto_nhdsWithin_Ioo_right

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_rightView on Github →