add — Mathlib

English

If f is Hölder with C and g is Hölder with C', then f+g is Hölder with C+C' and the same exponent r.

Русский

Если f Холдер с константой C, a g Холдер с константой C', то f+g Холдер с константой C+C' и тем же показателем r.

LaTeX

$$$\operatorname{HolderWith}(C,r,f) \land \operatorname{HolderWith}(C',r,g) \Rightarrow \operatorname{HolderWith}(C+C',r,f+g)$$$

Lean4

theorem add (hf : HolderWith C r f) (hg : HolderWith C' r g) : HolderWith (C + C') r (f + g) :=
  by
  intro x₁ x₂
  simp only [Pi.add_apply, coe_add]
  grw [edist_add_add_le, hf x₁ x₂, hg x₁ x₂]
  rw [add_mul]

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