toLinearIsometry — Mathlib

English

One can upgrade an isometric linear map to a linear isometry given a proof of isometry.

Русский

Можно превратить изометрическое линейное отображение в линейную изометрию при условии, что оно изометрично.

LaTeX

$$def toLinearIsometry (f : E →ₛₗ[σ₁₂] E₂) (hf : Isometry f) : E →ₛₗᵢ[σ₁₂] E₂ := { f with norm_map' := by simp_rw [← dist_zero_right] ; simpa using (hf.dist_eq · 0) }$$

Lean4

/-- Construct a `LinearIsometry` from a `LinearMap` satisfying `Isometry`. -/
def toLinearIsometry (f : E →ₛₗ[σ₁₂] E₂) (hf : Isometry f) : E →ₛₗᵢ[σ₁₂] E₂ :=
  { f with
    norm_map' := by
      simp_rw [← dist_zero_right]
      simpa using (hf.dist_eq · 0) }

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