isBounded_range_of_cauchy_map_cofinite

English

If f tends to infinity in the cofinite uniformity, then its range is bounded.

Русский

Если функция f стремится к бесконечности в рамках кофинитной равномерности, то её образ ограничен.

LaTeX

$$$\exists \text{...} \Rightarrow \operatorname{IsBounded}(\operatorname{range} f)$$$

Lean4

theorem isBounded_range_of_cauchy_map_cofinite {f : β → α} (hf : Cauchy (map f cofinite)) : IsBounded (range f) :=
  isBounded_range_of_tendsto_cofinite_uniformity <| (cauchy_map_iff.1 hf).2

Похожие утверждения