isometryOfInner — Mathlib

English

For a linear isometric equivalence f: E ≃ₗᵢ[𝕜] E', the adjoint equals the inverse up to canonical identifications: ⟪f x, y⟫ = ⟪x, f.symm y⟫.

Русский

Для линейной изометрической эквивалентности f: E ≃ₗᵢ[𝕜] E′ верно ⟪f x, y⟫ = ⟪x, f.symm y⟫.

LaTeX

$$$ \\langle f x, y \\rangle_𝕜 = \\langle x, f^{-1} y \\rangle_𝕜 $$$

Lean4

/-- A linear equivalence that preserves the inner product is a linear isometric equivalence. -/
def isometryOfInner (f : E ≃ₗ[𝕜] E') (h : ∀ x y, ⟪f x, f y⟫ = ⟪x, y⟫) : E ≃ₗᵢ[𝕜] E' :=
  ⟨f, ((f : E →ₗ[𝕜] E').isometryOfInner h).norm_map⟩

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