isBounded_range_of_tendsto_cofinite_uniformity

English

The same as isBounded_image_iff but expressed with simpler predicate structure.

Русский

То же самое, что и in isBounded_image_iff_simplified, выраженное через более простую структуру предикатов.

LaTeX

$$$IsBounded( f'' s) \iff \exists C, \forall x \in s, \forall y \in s, \operatorname{dist}(f x, f y) \le C$$$

Lean4

theorem isBounded_range_of_tendsto_cofinite_uniformity {f : β → α}
    (hf : Tendsto (Prod.map f f) (.cofinite ×ˢ .cofinite) (𝓤 α)) : IsBounded (range f) :=
  by
  rcases (hasBasis_cofinite.prod_self.tendsto_iff uniformity_basis_dist).1 hf 1 zero_lt_one with ⟨s, hsf, hs1⟩
  rw [← image_union_image_compl_eq_range]
  refine (hsf.image f).isBounded.union (isBounded_image_iff.2 ⟨1, fun x hx y hy ↦ ?_⟩)
  exact le_of_lt (hs1 (x, y) ⟨hx, hy⟩)

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