Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-09-18 15:31 ce64cd31

View on Github →

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 ℝⁿ.

Estimated changes