holderOnWith — Mathlib

English

If f is Hölder on X, then it is Hölder on any subset s.

Русский

Если функция f удовлетворяет условию Холдер на X, то она удовлетворяет его и на любом подмножестве s.

LaTeX

$$$\\forall s, \\operatorname{HolderOnWith} C r f s$ if $f$ is HolderWith C r f$$$

Lean4

protected theorem holderOnWith {C r : ℝ≥0} {f : X → Y} (h : HolderWith C r f) (s : Set X) : HolderOnWith C r f s :=
  fun x _ y _ => h x y

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