coe_symm_toHomeomorph

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The inverse of the homeomorph component of e equals the symm component of e.

Русский

Обратная сторона компонентa гомеоморфии e совпадает с симм-частью e.

LaTeX

$$$ (e.toHomeomorph)^{-1} = e.symm $$$

Lean4

@[simp]
theorem coe_symm_toHomeomorph : ⇑e.toHomeomorph.symm = e.symm :=
  rfl

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

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

Разделы

Аффилиация

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