coe_restrictScalars — Mathlib

English

Let p be a seminorm on E viewed as a vector space over 𝕜'. When we restrict scalars to 𝕜, the resulting seminorm on E is the same function as p. In particular, for all x in E, (p.restrictScalars 𝕜)(x) = p(x).

Русский

Пусть p — семинорм на E, рассматриваемом какекторное пространство над 𝕜'. При ограничении скаляров до 𝕜 полученная семинормa на E совпадает с p: для каждого x ∈ E верно (p.restrictScalars 𝕜)(x) = p(x).

LaTeX

$$$ (p\\restrictScalars 𝕜) = p \\quad \\text{as functions } E \\to \\mathbb{R}. $$$

Lean4

@[simp]
theorem coe_restrictScalars (p : Seminorm 𝕜' E) : (p.restrictScalars 𝕜 : E → ℝ) = p :=
  rfl

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