mathlib

ce64cd31 - feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (#18629)

feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (#18629) Generalise `bounded_le_nhds`/`bounded_ge_nhds` using two ad hoc typeclasses. The goal here is to circumvent the fact that the product of order topologies is *not* an order topology, and apply those lemmas to `ℝⁿ`.