Commit 2026-04-28 16:44 44a8ac64

feat(Topology/Order/Bornology): generalize cobounded_eq (#37738) Real.cobounded_eq and Int.cobounded_eq are used in several places throughout Mathlib. They are currently proved in terms of the Metric topology on Int and Real, but they're really properties of the order bornology on those objects. Generalize those constructions to IsOrderBornology for LinearOrder's and add a few more constructions that are true in other circumstances, e.g., cobounded NNReal = .atTop follows from the fact that NNReal is both NoMaxOrder and OrderBot.