Theorem nonempty_nhds_inter_Iio

Modification history

2026-10-05 09:13
Mathlib/Topology/Order/DenselyOrdered.lean
feat: tag `Function.leftLim` with `to_dual` (#43525)
Deleted nonempty_nhds_inter_IioView on Github →
2026-04-07 12:09
Mathlib/Topology/Order/DenselyOrdered.lean
feat(Topology/Order): add `IsMax.of_disjoint_nhds_Ioi`, `IsMin.of_disjoint_nhds_Iio`, `nonempty_nhds_inter_Ioi`, `nonempty_nhds_inter_Iio` (#37550) …
Added nonempty_nhds_inter_IioView on Github →