locallyLipschitzOn_empty

Mathlib.Topology.EMetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#locallyLipschitzOn_empty

English

A function is locally Lipschitz on the empty set (trivially true).

Русский

Функция локально Lipschitz на пустом множестве тривиальна.

LaTeX

$$LocallyLipschitzOn(\emptyset, f)$$

Lean4

@[simp]
theorem locallyLipschitzOn_empty (f : α → β) : LocallyLipschitzOn ∅ f := fun _ ↦ False.elim

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

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

Разделы

Аффилиация

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