Documentation

Mathlib.Topology.Bornology.Real

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.

source
instance Real.instIsOrderBornology :
IsOrderBornology ℝ
source
instance NNReal.instOrderTopology :
OrderTopology NNReal
source
instance NNReal.instIsOrderBornology :
IsOrderBornology NNReal