uniformContinuousOn_of_continuous

English

If s is compact and f is continuous on s, then f is UniformContinuousOn f s.

Русский

Если s компактно, и f непрерывна на s, то f равномерно непрерывна на s.

LaTeX

$$\\text{If } IsCompact(s) \\text{ and } ContinuousOn(f,s) \\text{ then } UniformContinuousOn(f,s).$$

Lean4

/-- Heine-Cantor: a continuous function on a compact set of a uniform space is uniformly
continuous. -/
theorem uniformContinuousOn_of_continuous {s : Set α} {f : α → β} (hs : IsCompact s) (hf : ContinuousOn f s) :
    UniformContinuousOn f s := by
  rw [uniformContinuousOn_iff_restrict]
  rw [isCompact_iff_compactSpace] at hs
  rw [continuousOn_iff_continuous_restrict] at hf
  exact CompactSpace.uniformContinuous_of_continuous hf

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