Relating order and metric boundedness

In spaces equipped with both an order and a metric, there are separate notions of boundedness associated with each of the two structures. In specific cases such as ℝ, there are results which relate the two notions.

Tags

bounded, bornology, order, metric

theorem Filter.isBounded_le_map_of_bounded_range {ι : Type u_1} (F : Filter ι) {f : ι → ℝ} (h : Bornology.IsBounded (Set.range f)) : Filter.IsBounded (fun (x x_1 : ℝ) => x ≤ x_1) (Filter.map f F)

theorem Filter.isBounded_ge_map_of_bounded_range {ι : Type u_1} (F : Filter ι) {f : ι → ℝ} (h : Bornology.IsBounded (Set.range f)) : Filter.IsBounded (fun (x x_1 : ℝ) => x ≥ x_1) (Filter.map f F)