tendsto — Mathlib

English

If x is a cluster point for lx and f is continuous at x and tends to ly along lx, then ClusterPt(f(x)) along ly.

Русский

Если x — кластерная точка относительно lx и f непрерывна в x и стремится к ly вдоль lx, тогда ClusterPt(f(x)) относительно ly.

LaTeX

$$$\\text{ClusterPt}(x, lx) \\rightarrow \\mathrm{ContinuousAt}(f, x) \\rightarrow \\mathrm{Tendsto}(f, lx, ly) \\rightarrow \\text{ClusterPt}(f x, ly)$$$

Lean4

theorem tendsto (hf : Continuous f) (x) : Tendsto f (𝓝 x) (𝓝 (f x)) :=
  ((nhds_basis_opens x).tendsto_iff <| nhds_basis_opens <| f x).2 fun t ⟨hxt, ht⟩ =>
    ⟨f ⁻¹' t, ⟨hxt, ht.preimage hf⟩, Subset.rfl⟩

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