inner_map_map — Mathlib

English

A linear isometric equivalence f: E ≃ₗᵢ[𝕜] E' preserves the inner product: ⟪f x, f y⟫ = ⟪x, y⟫ for all x,y ∈ E.

Русский

Линейная изометрическая эквиваленция f сохраняет скалярное произведение: для всех x,y ∈ E верно ⟪f x, f y⟫ = ⟪x, y⟫.

LaTeX

$$$ \\forall x,y:\\ E, \\< f x, f y \\>_𝕜 = \\< x, y \\>_𝕜 $$$

Lean4

/-- A linear isometric equivalence preserves the inner product. -/
@[simp]
theorem inner_map_map (f : E ≃ₗᵢ[𝕜] E') (x y : E) : ⟪f x, f y⟫ = ⟪x, y⟫ :=
  f.toLinearIsometry.inner_map_map x y

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