mono — Mathlib

English

If f is Hölder with constant C, then it is Hölder with any larger constant C' ≥ C.

Русский

Если функция Холдер с константой C, то она также Холдер с любой константой C' ≥ C.

LaTeX

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

Lean4

theorem mono {C' : ℝ≥0} (hf : HolderWith C r f) (h : C ≤ C') : HolderWith C' r f := fun x₁ x₂ ↦
  (hf x₁ x₂).trans (mul_left_mono (coe_le_coe.2 h))

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