eHolderNorm_lt_top — Mathlib

English

Let X,Y be spaces with a pseudo-emetric structure. For r ≥ 0 and f: X → Y, eHolderNorm r f is finite if and only if f satisfies the Hölder condition MemHolder r f.

Русский

Пусть X,Y — пространства с псевдо-эметрическим расстоянием. Для r ≥ 0 и f: X → Y.normHolder нормa eHolderNorm r f конечна тогда и только тогда, когда f удовлетворяет условию Холлера MemHolder r f.

LaTeX

$$$eHolderNorm(r,f) < \infty \iff \operatorname{MemHolder}(r,f).$$$

Lean4

@[simp]
theorem eHolderNorm_lt_top : eHolderNorm r f < ∞ ↔ MemHolder r f :=
  by
  refine
    ⟨fun h => ?_, fun hf =>
      let ⟨C, hC⟩ := hf;
      iInf_lt_top.2 ⟨C, iInf_lt_top.2 ⟨hC, coe_lt_top⟩⟩⟩
  simp_rw [eHolderNorm, iInf_lt_top] at h
  let ⟨C, hC, _⟩ := h
  exact ⟨C, hC⟩

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