The reals are equipped with their order bornology

This file contains results related to the order bornology on (non-negative) real numbers. We prove that ℝ and ℝ≥0 are equipped with the order topology and bornology.

instance instIsOrderBornology : IsOrderBornology ℝ

Every instance is inherited from the corresponding structures on the reals.

instance NNReal.instOrderTopology : OrderTopology NNReal

instance NNReal.instIsOrderBornology : IsOrderBornology NNReal