inner_map_map — Mathlib

English

A linear isometry f preserves the inner product: ⟪f x, f y⟫ = ⟪x, y⟫ for all x,y.

Русский

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

LaTeX

$$$ \\forall x,y:\\ V, \\ \\langle f x, f y \\rangle = \\langle x, y \\rangle $$$

Lean4

/-- A linear isometry preserves the inner product. -/
@[simp]
theorem inner_map_map (f : E →ₗᵢ[𝕜] E') (x y : E) : ⟪f x, f y⟫ = ⟪x, y⟫ := by
  simp [inner_eq_sum_norm_sq_div_four, ← f.norm_map]

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