continuousOn

Mathlib.Topology.EMetricSpace.Lipschitz

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

English

A Lipschitz-on-a-set function is continuous-on-that-set.

Русский

ЛипшитсOnWith обеспечивает непрерывность на множестве.

LaTeX

$$$\\text{LipschitzOnWith } K f s \\Rightarrow \\text{ ContinuousOn } f s$$$

Lean4

protected theorem continuousOn (hf : LipschitzOnWith K f s) : ContinuousOn f s :=
  hf.uniformContinuousOn.continuousOn

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

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

Разделы

Аффилиация

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