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

@[deprecated Filter.isBoundedUnder_of (since := "2024-06-07")]

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

@[deprecated Filter.isBoundedUnder_of (since := "2024-06-07")]

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