ext_linearIsometryEquiv — Mathlib

English

Two linear isometric equivalences are equal if they agree on the images of basis vectors.

Русский

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

LaTeX

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

Lean4

/-- Two linear isometric equivalences are equal if they are equal on basis vectors. -/
theorem ext_linearIsometryEquiv {ι : Type*} (b : Basis ι R E) {f₁ f₂ : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ i, f₁ (b i) = f₂ (b i)) :
    f₁ = f₂ :=
  LinearIsometryEquiv.toLinearEquiv_injective <| b.ext' h

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