continuousOn

Mathlib.Topology.EMetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#LocallyLipschitzOn.continuousOn

English

If f is locally Lipschitz on a set s, then f is continuous on s.

Русский

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

LaTeX

$$$\\forall f\\,s,\\ LocallyLipschitzOn\\,s\\,f\\Rightarrow ContinuousOn\\,f\\,s$$$

Lean4

protected theorem continuousOn (hf : LocallyLipschitzOn s f) : ContinuousOn f s :=
  continuousOn_iff_continuous_restrict.2 hf.restrict.continuous

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru