coe_symm_toIsometryEquiv

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The inverse of the isometry equivalence obtained from e has the same underlying map as e.symm.

Русский

Обратное отображение киеquivalence из e имеет ту же самую базовую карту как и e.symm.

LaTeX

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

Lean4

@[simp]
theorem coe_symm_toIsometryEquiv : ⇑e.toIsometryEquiv.symm = e.symm :=
  rfl

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

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

Разделы

Аффилиация

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