Theorem MonotoneOn.tendsto_nhdsWithin_Ioi

Modification history

2024-12-23 08:37

Mathlib/Topology/Order/Monotone.lean

chore(*): rename lemmas about `𝓝[≥] a` etc (#20188) …

Deleted MonotoneOn.tendsto_nhdsWithin_Ioi View on Github →

2024-08-19 18:48

Mathlib/Topology/Order/Monotone.lean

feat (Topology.Order): Generalize `Monotone.tendsto_nhdsWithin_Iio` (#15470) …

Added MonotoneOn.tendsto_nhdsWithin_Ioi View on Github →