bijective

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The map underlying a LinearIsometryEquiv is bijective; its inverse is e.symm.

Русский

Обозначение линейной изометрической эквивалентности является биективным; его обратное — e.symm.

LaTeX

$$$ e \text{ is bijective and } e^{-1} = e^{\mathrm{symm}} $$$

Lean4

protected theorem bijective : Bijective e :=
  e.1.bijective

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

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

Разделы

Аффилиация

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