continuous

Mathlib.Topology.MetricSpace.Holder

URI: https://scilib.ai/kg/mathlib#HolderWith.continuous

English

A constant function is Hölder with any constants C,r on any domain.

Русский

Постоянная функция Холдер с любыми константами на любой области.

LaTeX

$$$\operatorname{HolderWith}(C,r,\text{const}_X\;y)$$$

Lean4

protected theorem continuous (hf : HolderWith C r f) (h0 : 0 < r) : Continuous f :=
  (hf.uniformContinuous h0).continuous

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

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

Разделы

Аффилиация

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