toLinearMap_inj

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometry.toLinearMap_inj

English

If two semilinear isometries agree on every vector, then they are equal.

Русский

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

LaTeX

$$$\forall x,\ f(x)=g(x) \implies f=g$$$

Lean4

@[simp]
theorem toLinearMap_inj {f g : E →ₛₗᵢ[σ₁₂] E₂} : f.toLinearMap = g.toLinearMap ↔ f = g :=
  toLinearMap_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru