memHolder — Mathlib

English

If a function f: X → Y between spaces with a pseudo-emetric structure satisfies a Hölder condition with exponent r and constant C, then f is MemHolder r f (i.e., it has a Hölder bound with the same data).

Русский

Если функция f: X → Y удовлетворяет условию Холлера с показателем r и константой C, то f принадлежит MemHolder r f (то есть обладает тем же Hölder-ограничением).

LaTeX

$$$\operatorname{HolderWith}(C,r,f) \Rightarrow \operatorname{MemHolder}(r,f)$$$

Lean4

theorem memHolder {C : ℝ≥0} (hf : HolderWith C r f) : MemHolder r f :=
  ⟨C, hf⟩

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