continuousOn_univ — Mathlib

English

A function is continuous on the whole space if and only if it is globally continuous.

Русский

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

LaTeX

$$$ \text{ContinuousOn } f \operatorname{univ} \iff \text{Continuous } f $$$

Lean4

@[simp]
theorem continuousOn_univ {f : α → β} : ContinuousOn f univ ↔ Continuous f := by
  simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]

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