ContinuousWithinAt — Mathlib

English

A function f: X → Y is continuous at x within a subset s ⊆ X if Tendsto f (nhdsWithin x s) (nhds (f x)).

Русский

Функция f: X → Y непрерывна в точке x относительно множества s ⊆ X, если Tendsto f (nhdsWithin x s) (nhds (f x)).

LaTeX

$$$\operatorname{ContinuousWithinAt}(f,s,x) \iff \operatorname{Tendsto} f (\\nhdsWithin x s) (\\nhds (f x))$$$

Lean4

/-- A function between topological spaces is continuous at a point `x₀` within a subset `s`
if `f x` tends to `f x₀` when `x` tends to `x₀` while staying within `s`. -/
@[fun_prop]
def ContinuousWithinAt (f : X → Y) (s : Set X) (x : X) : Prop :=
  Tendsto f (𝓝[s] x) (𝓝 (f x))

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