holderOnWith_empty

Mathlib.Topology.MetricSpace.Holder

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

English

HolderOnWith with any constants on the empty set holds vacuously.

Русский

Условие Холдер на пустом множестве выполняется вакуумно для любых констант.

LaTeX

$$$\\text{HolderOnWith } C r f \\emptyset$$$

Lean4

@[simp]
theorem holderOnWith_empty (C r : ℝ≥0) (f : X → Y) : HolderOnWith C r f ∅ := fun _ hx => hx.elim

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

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

Разделы

Аффилиация

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