continuousAt_def — Mathlib

English

A function f is continuous at x iff for every neighborhood A of f(x), the preimage f^{-1}(A) is a neighborhood of x.

Русский

Функция f непрерывна в x тогда и только тогда, когда для каждого окрестности A точки f(x) её прообраз f^{-1}(A) является окрестностью x.

LaTeX

$$$\mathrm{ContinuousAt}(f, x) \iff \forall A \in 𝓝 (f x), f^{-1}(A) \in 𝓝 x.$$$

Lean4

theorem continuousAt_def : ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x :=
  Iff.rfl

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