norm_map_iff_inner_map_map — Mathlib

English

A linear map f preserves norms if and only if it preserves inner products: ∥f x∥ = ∥x∥ for all x ⇔ ∀ x,y, ⟪f x, f y⟫ = ⟪x, y⟫.

Русский

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

LaTeX

$$$( \\forall x:\\ E, \\|f x\\| = \\|x\\|) \\iff ( \\forall x,y:\\ E, \\langle f x, f y \\rangle = \\langle x, y \\rangle)$$$

Lean4

/-- A linear map is an isometry if and it preserves the inner product. -/
theorem norm_map_iff_inner_map_map {F : Type*} [FunLike F E E'] [LinearMapClass F 𝕜 E E'] (f : F) :
    (∀ x, ‖f x‖ = ‖x‖) ↔ (∀ x y, ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜) :=
  ⟨({ toLinearMap := LinearMapClass.linearMap f, norm_map' := · : E →ₗᵢ[𝕜] E' }.inner_map_map),
    (LinearMapClass.linearMap f |>.isometryOfInner · |>.norm_map)⟩

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