coe_toLinearMap

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometry.coe_toLinearMap

English

Reiteration: the ContinuousSemilinearMapClass is furnished by the existing continuity of semilinear isometries.

Русский

Повторно: ContinuousSemilinearMapClass обеспечивается непрерывностью семилинейных изометрий.

LaTeX

$$$\text{ContinuousSemilinearMapClass}(\mathcal{F},\sigma_{12},E,E_2)$$$

Lean4

@[simp]
theorem coe_toLinearMap : ⇑f.toLinearMap = f :=
  rfl

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

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

Разделы

Аффилиация

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