innerProductSpace — Mathlib

English

The induced inner product on a subspace W of E defines an inner product space structure on W.

Русский

Унаследованное скалярное произведение на подпространстве W пространства E образует скалярное произведение на W.

LaTeX

$$InnerProductSpace 𝕜 W with ⟪x,y⟫_W = ⟪x,y⟫_E$$

Lean4

/-- Induced inner product on a submodule. -/
instance innerProductSpace (W : Submodule 𝕜 E) : InnerProductSpace 𝕜 W :=
  { Submodule.normedSpace W with
    inner := fun x y => ⟪(x : E), (y : E)⟫
    conj_inner_symm := fun _ _ => inner_conj_symm _ _
    norm_sq_eq_re_inner := fun x => norm_sq_eq_re_inner (x : E)
    add_left := fun _ _ _ => inner_add_left _ _ _
    smul_left := fun _ _ _ => inner_smul_left _ _ _ }

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