Theorem Real.cobounded_eq

Modification history

2026-04-28 16:44
Mathlib/Topology/Instances/Real/Lemmas.lean
feat(Topology/Order/Bornology): generalize `cobounded_eq` (#37738) …
Deleted Real.cobounded_eqView on Github →
2023-10-06 14:17
Mathlib/Topology/Instances/Real.lean
refactor(MetricSpace/Basic): use `cobounded` more (#7543)
Added Real.cobounded_eqView on Github →