toContinuousLinearMap_injective — Mathlib

English

If two linear isometries have the same associated continuous linear map, then the two isometries are equal.

Русский

Если две линейные изометрии имеют одинаковое сопутствующее непрерывное линейное отображение, то они равны.

LaTeX

$$f.toContinuousLinearMap = g.toContinuousLinearMap → f = g$$

Lean4

theorem toContinuousLinearMap_injective : Function.Injective (toContinuousLinearMap : _ → E →SL[σ₁₂] E₂) := fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toContinuousLinearMap = _)

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