self_trans_symm

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometryEquiv.self_trans_symm

English

The symmetric of a composed equivalence is the composition of the symmetric of the second with the symmetric of the first.

Русский

Обратное составленного эквивалента равно композиции симм второго и симм первого.

LaTeX

$$$ (e.trans e').symm = e'.symm.trans e.symm $$$

Lean4

@[simp]
theorem self_trans_symm : e.trans e.symm = refl R E :=
  ext e.symm_apply_apply

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

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

Разделы

Аффилиация

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