ext_linearIsometry — Mathlib

English

Two linear isometries are equal if they agree on the images of all basis vectors.

Русский

Две линейные изометрии равны, если они совпадают на образах всех базисных векторов.

LaTeX

$$$\forall i, f_1(b_i) = f_2(b_i)\Rightarrow f_1 = f_2$$$

Lean4

/-- Two linear isometries are equal if they are equal on basis vectors. -/
theorem ext_linearIsometry {ι : Type*} (b : Basis ι R E) {f₁ f₂ : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ i, f₁ (b i) = f₂ (b i)) :
    f₁ = f₂ :=
  LinearIsometry.toLinearMap_injective <| b.ext h

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