locallyLipschitzOn_iff_continuousOn

English

The continuousOn property for ConcaveOn follows from its local Lipschitz property.

Русский

Свойство непрерывности для ConcaveOn следует из локальной липшицевости.

LaTeX

$$$ \\text{ConcaveOn.continuousOn} $$$

Lean4

theorem locallyLipschitzOn_iff_continuousOn (hC : IsOpen C) (hf : ConcaveOn ℝ C f) :
    LocallyLipschitzOn C f ↔ ContinuousOn f C := by simpa using hf.neg.locallyLipschitzOn_iff_continuousOn hC

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