instCoeFunForallENNReal — Mathlib

English

There is a canonical way to view an extended-normed space as a function from V to the extended nonnegative reals, given by x maps to e(x).

Русский

Существует канонический способ рассматривать расширенное нормированное пространство как функцию от V в\\mathbb{R}_{\\ge 0}^{\\infty}, задаваемую x ↦ e(x).

LaTeX

$$$(\\widehat{e}: V \\to \\mathbb{R}_{\\ge 0}^{\\infty}) \\text{ defined by } \\widehat{e}(x) = e(x).$$$

Lean4

instance : CoeFun (ENormedSpace 𝕜 V) fun _ => V → ℝ≥0∞ :=
  ⟨ENormedSpace.toFun⟩

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