continuous_iff_continuousAt — Mathlib

English

A function is continuous iff it is continuous at every point.

Русский

Функция непрерывна тогда и только тогда, когда она непрерывна в каждой точке.

LaTeX

$$$\\mathrm{Continuous}(f) \\iff \\forall x, \\mathrm{ContinuousAt}(f, x)$$$

Lean4

theorem continuous_iff_continuousAt : Continuous f ↔ ∀ x, ContinuousAt f x :=
  ⟨Continuous.tendsto, fun hf => continuous_def.2 fun _U hU => isOpen_iff_mem_nhds.2 fun x hx => hf x <| hU.mem_nhds hx⟩

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