self_comp_symm

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The inverse of the composed map equals the composition of the inverses in reverse order.

Русский

Обратное композиции равно композиции обратных в обратном порядке.

LaTeX

$$$ (e_1 \\trans e_2)^{-1} = e_2^{-1} \\trans e_1^{-1} $$$

Lean4

@[simp]
theorem self_comp_symm : e ∘ e.symm = id :=
  e.symm.symm_comp_self

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

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

Разделы

Аффилиация

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