ContinuousAt — Mathlib

English

A function between topological spaces is continuous at a point x0 if f(x) tends to f(x0) whenever x tends to x0.

Русский

Функция между топологическими пространствами непрерывна в точке x0, если x → x0 тогда f(x) → f(x0).

LaTeX

$$$\text{ContinuousAt}(f,x) \iff \operatorname{Tendsto} f (\\mathcal{N} x) (\\mathcal{N}(f x))$$$

Lean4

/-- A function between topological spaces is continuous at a point `x₀`
if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
@[fun_prop]
def ContinuousAt (f : X → Y) (x : X) :=
  Tendsto f (𝓝 x) (𝓝 (f x))

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