continuousAt_iff_ultrafilter — Mathlib

English

A function f is continuous at x if and only if for every ultrafilter g on X with g ≤ 𝓝 x, Tendsto f g (𝓝 (f x)).

Русский

Функция f непрерывна в точке x тогда и только тогда, для каждого ультрафильтра g на X с g ≤ 𝓝 x, выполнено Tendsto f g (𝓝 (f x)).

LaTeX

$$$\\text{ContinuousAt}(f,x) \\iff \\forall g : Ultrafilter X, g \\le 𝓝 x \\rightarrow Tendsto(f,g,𝓝(f(x)))$$$

Lean4

theorem continuousAt_iff_ultrafilter : ContinuousAt f x ↔ ∀ g : Ultrafilter X, ↑g ≤ 𝓝 x → Tendsto f g (𝓝 (f x)) :=
  tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x))

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