memHolder_const — Mathlib

English

From MemHolder r f one obtains HolderWith (nnHolderNorm r f) r f.

Русский

Из MemHolder r f следует HolderWith (nnHolderNorm r f) r f.

LaTeX

$$$\operatorname{MemHolder}(r,f) \Rightarrow \operatorname{HolderWith}(\mathrm{nnHolderNorm}(r,f), r, f).$$$

Lean4

/-- See also `memHolder_const` for the version with the spelling `fun _ ↦ c`. -/
@[simp]
theorem memHolder_const {c : Y} : MemHolder r (Function.const X c) :=
  (HolderWith.const (C := 0)).memHolder

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