continuousOn — Mathlib

English

If a function is uniformly continuous on a set, then it is continuous on that set.

Русский

Если функция равномерно непрерывна на множестве, то она непрерывна на этом множестве.

LaTeX

$$$$\\text{UniformContinuousOn } f s\\Rightarrow \\text{ContinuousOn } f s.$$$$

Lean4

theorem continuousOn [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} (h : UniformContinuousOn f s) :
    ContinuousOn f s := by
  rw [uniformContinuousOn_iff_restrict] at h
  rw [continuousOn_iff_continuous_restrict]
  exact h.continuous

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