holderWith_zero_iff — Mathlib

English

For metric spaces, HolderWith 0 r f is equivalent to f being constant.

Русский

Для метрических пространств Holders 0 означает, что функция константна.

LaTeX

$$$\operatorname{HolderWith}(0,r,f) \iff \forall x_1,x_2,\ f(x_1)=f(x_2)$$$

Lean4

@[simp]
theorem holderWith_zero_iff : HolderWith 0 r f ↔ ∀ x₁ x₂, f x₁ = f x₂ :=
  by
  refine ⟨fun h x₁ x₂ => ?_, fun h x₁ x₂ => h x₁ x₂ ▸ ?_⟩
  · specialize h x₁ x₂
    simp [ENNReal.coe_zero, zero_mul, nonpos_iff_eq_zero, edist_eq_zero] at h
    assumption
  · simp only [edist_self, ENNReal.coe_zero, zero_mul, le_refl]

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