comp

Mathlib.Topology.MetricSpace.HolderNorm

URI: https://scilib.ai/kg/mathlib#MemHolder.comp

← MathLib Explorer

English

Similarly, eHolderNorm r f ≤ C holds for HolderWith C r f.

Русский

Аналогично, если f удовлетворяет HolderWith, то eHolderNorm r f ≤ C.

LaTeX

$$$eHolderNorm(r,f) \le \operatorname{ofNNReal}(C).$$$

Lean4

theorem comp {r s : ℝ≥0} {Z : Type*} [MetricSpace Z] {f : Z → X} {g : X → Y} (hf : MemHolder r f) (hg : MemHolder s g) :
    MemHolder (s * r) (g ∘ f) :=
  (hg.holderWith.comp hf.holderWith).memHolder

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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