toContinuousLinearMap_inj — Mathlib

English

There exists an equivalence: two linear isometries are equal if and only if their associated continuous linear maps are equal.

Русский

Существует эквивалентность: две линейные изометрии равны тогда и только тогда, когда их сопутствующие непрерывные линейные отображения равны.

LaTeX

$$f.toContinuousLinearMap = g.toContinuousLinearMap ⇔ f = g$$

Lean4

@[simp]
theorem toContinuousLinearMap_inj {f g : E →ₛₗᵢ[σ₁₂] E₂} : f.toContinuousLinearMap = g.toContinuousLinearMap ↔ f = g :=
  toContinuousLinearMap_injective.eq_iff

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