innerₗ_apply — Mathlib

English

Equivalence of norm preservation and inner-product preservation as in the linear-map norm criterion.

Русский

Сопряжённость сохранения нормы и сохранения скалярного произведения как критерий линейного отображения.

LaTeX

$$$ (\\forall x, \\|f x\\| = \\|x\\|) \\iff (\\forall x,y, ⟪f x, f y⟫ = ⟪x,y⟫) $$$

Lean4

@[simp]
theorem innerₗ_apply (v w : F) : innerₗ F v w = ⟪v, w⟫_ℝ :=
  rfl

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