Documentation

Mathlib.Topology.Order.Bounded

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]
theorem Filter.isBounded_le_map_of_bounded_range {ι : Type u_1} (F : Filter ι) {f : ι} (h : Bornology.IsBounded (Set.range f)) :
Filter.IsBounded (fun (x1 x2 : ) => x1 x2) (Filter.map f F)
@[deprecated Filter.isBoundedUnder_of]
theorem Filter.isBounded_ge_map_of_bounded_range {ι : Type u_1} (F : Filter ι) {f : ι} (h : Bornology.IsBounded (Set.range f)) :
Filter.IsBounded (fun (x1 x2 : ) => x1 x2) (Filter.map f F)