finite_norm_eq — Mathlib

English

Let e be a normed space structure on the finite-subspace e.finiteSubspace of V. Then for every x in e.finiteSubspace, the norm of x computed in e agrees with the real norm coming from e, i.e. ‖x‖ = (e x).toReal.

Русский

Пусть e задаёт нормированное пространство на конечном подпространстве e.finiteSubspace V. Тогда для любого x из e.finiteSubspace нормa x, взятая в рамках e, совпадает с вещественной нормой, получаемой из e: ‖x‖ = (e x).toReal.

LaTeX

$$$\\|x\\| = (e\\,x).toReal \\quad (x \\in e.finiteSubspace)$$$

Lean4

@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]
theorem finite_norm_eq (x : e.finiteSubspace) : ‖x‖ = (e x).toReal :=
  rfl

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