continuousOn_iff — Mathlib

English

If for every x in s we have ContinuousAt f x, then ContinuousOn f s.

Русский

Если для каждого x в s верна непрерывность f в x, то f непрерывна на s.

LaTeX

$$$$\bigl(\forall x\,(x\in s \to \text{ContinuousAt}(f,x))\bigr) \Rightarrow \text{ContinuousOn}(f,s)$$$$

Lean4

theorem continuousOn_iff (hs : IsOpen s) : ContinuousOn f s ↔ ∀ ⦃a⦄, a ∈ s → ContinuousAt f a :=
  forall₂_congr fun _ => continuousWithinAt_iff_continuousAt ∘ hs.mem_nhds

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