tendsto_iff_dist_tendsto_zero — Mathlib

English

For any f:β→α, Tendsto f x (nhds a) iff Tendsto (λ b, dist (f b) a) x (nhds 0).

Русский

Для любой f:β→α справедливо равенство: сходимость f к a эквивалентна сходимостиdistance(f b, a) к 0.

LaTeX

$$$\operatorname{Tendsto} f\ x\ (\mathcal N a) \iff \operatorname{Tendsto}(\lambda b. \operatorname{dist}(f b, a))\ x\ (\mathcal N 0)$$$

Lean4

theorem tendsto_iff_dist_tendsto_zero {f : β → α} {x : Filter β} {a : α} :
    Tendsto f x (𝓝 a) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0) := by
  rw [← nhds_comap_dist a, tendsto_comap_iff, Function.comp_def]

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