tendsto_nhds_iff — Mathlib

English

Tendsto is preserved by a uniform inducing dilation: Tendsto g a to nhds b iff Tendsto (f ∘ g) a to nhds (f b).

Русский

Пределимость в окрестностях сохраняется дилатацией; Tendsto g к nhds b эквивалентно Tendsto (f∘g) к nhds (f b).

LaTeX

$$$\\operatorname{Tendsto}\ g\ a\ \\mathcal{N}(b) \\iff \\operatorname{Tendsto}\ (f \\circ g)\ a\\ \\mathcal{N}(f(b))$$$

Lean4

theorem tendsto_nhds_iff {ι : Type*} {g : ι → α} {a : Filter ι} {b : α} :
    Filter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto ((f : α → β) ∘ g) a (𝓝 (f b)) :=
  (Dilation.isUniformInducing f).isInducing.tendsto_nhds_iff

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