tendsto_nhds — Mathlib

English

A function f tends to x along l if and only if preimages of open sets around x lie in l.

Русский

Функция f стремится к x относительно фильтра l тогда, когда предобраза открытых множеств вокруг x принадлежат l.

LaTeX

$$$\\text{Tendsto } f\\ l\\ (\\mathcal N_x) \\iff \\forall s,\\ IsOpen(s) \\land x \\in s \\Rightarrow f^{-1}(s) \\in l.$$$

Lean4

theorem tendsto_nhds {f : α → X} {l : Filter α} : Tendsto f l (𝓝 x) ↔ ∀ s, IsOpen s → x ∈ s → f ⁻¹' s ∈ l :=
  all_mem_nhds_filter _ _ (fun _ _ h => preimage_mono h) _

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