locallyLipschitzOn_iff_continuousOn

English

For an open set C and convexOn function f, locally Lipschitz on C is equivalent to continuous on C.

Русский

Для открытого множества C и выпуклой функции f локальная липшицевость на C эквивалентна непрерывности на C.

LaTeX

$$$ LocallyLipschitzOn C f \\leftrightarrow ContinuousOn f C $$$

Lean4

theorem locallyLipschitzOn_iff_continuousOn (hC : IsOpen C) (hf : ConvexOn ℝ C f) :
    LocallyLipschitzOn C f ↔ ContinuousOn f C :=
  by
  obtain rfl | hC' := C.eq_empty_or_nonempty
  · simp
  · exact (hf.continuousOn_tfae hC hC').out 0 1

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