exists_isBounded_image_of_tendsto

English

If f: α → β and f tends to x along a filter l, there exists s ∈ l such that f''s is bounded.

Русский

Если f: α → β стремится к x вдоль фильтра l, существует множество s ∈ l такое, что образ f''s ограничен.

LaTeX

$$$\\\\forall l:\\\\text{Filter} α, f: α \\\\to β, x: β, \\\\ Tendsto f l (nhds x) \\\\Rightarrow \\\\exists s \\in l, IsBounded(f''s).$$$

Lean4

theorem exists_isBounded_image_of_tendsto {α β : Type*} [PseudoMetricSpace β] {l : Filter α} {f : α → β} {x : β}
    (hf : Tendsto f l (𝓝 x)) : ∃ s ∈ l, IsBounded (f '' s) :=
  (l.basis_sets.map f).disjoint_iff_left.mp <| (disjoint_nhds_cobounded x).mono_left hf

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