Theorem Set.OrdConnected.mem_nhdsWithin_Iio

Modification history

2024-12-23 08:37
Mathlib/Topology/Order/LeftRightNhds.lean
chore(*): rename lemmas about `𝓝[≥] a` etc (#20188) …
Deleted Set.OrdConnected.mem_nhdsWithin_IioView on Github →
2024-04-08 14:57
Mathlib/Topology/Order/LeftRightNhds.lean
feat(Analysis/Convex/Deriv): convex implies monotone deriv (#11602) …
Added Set.OrdConnected.mem_nhdsWithin_IioView on Github →