Commit 2026-04-07 12:09 7b476a17
View on Github →feat(Topology/Order): add IsMax.of_disjoint_nhds_Ioi, IsMin.of_disjoint_nhds_Iio, nonempty_nhds_inter_Ioi, nonempty_nhds_inter_Iio (#37550)
Add nonempty_nhds_inter_Ioi: a neighborhood of x has nonempty intersection with Ioi x when x is not a maximum.
Upstreamed from the Carleson project.