tendsto_nhds_iff — Mathlib

English

Tendsto through an isometry is equivalent to tendsto of the composed map.

Русский

Сходимость в окрестностях через изометрию эквивалентна сходности через композицию.

LaTeX

$$$Isometry\\ f \\Rightarrow \\forall g,a,b, Tendsto g\\ a\\ (nhds b) \\leftrightarrow Tendsto (f \\circ g)\\ a\\ (nhds (f b))$$$

Lean4

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

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