mono

Mathlib.Topology.MetricSpace.Holder

URI: https://scilib.ai/kg/mathlib#HolderOnWith.mono

English

If t ⊆ s, then Hölder continuity on s implies Hölder continuity on t with the same constants.

Русский

Если t ⊆ s, то Hölder на s ⇒ Hölder на t с теми же константами.

LaTeX

$$$\\text{HolderOnWith } C r f s \\;\\land\\; t \\subseteq s \\Rightarrow \\text{HolderOnWith } C r f t$$$

Lean4

protected theorem mono (hf : HolderOnWith C r f s) (ht : t ⊆ s) : HolderOnWith C r f t := fun _ hx _ hy =>
  hf.edist_le (ht hx) (ht hy)

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

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

Разделы

Аффилиация

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