Theorem IsMax.of_disjoint_nhds_Ioi

Modification history

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 IsMax.of_disjoint_nhds_IoiView on Github →