isometry_mul

Mathlib.Analysis.Normed.Operator.Mul

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.isometry_mul

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

theorem isometry_mul : Isometry (mul 𝕜 R) :=
  RegularNormedAlgebra.isometry_mul'

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

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

Разделы

Аффилиация

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