coe_toLinearIsometry

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

Theorem: Two LinearIsometryEquiv are equal iff their toLinearIsometry are equal.

Русский

Теорема: две LinearIsometryEquiv равны тогда и только тогда, когда их toLinearIsometry равны.

LaTeX

$$$\\forall f,g,\\; f.toLinearIsometry = g.toLinearIsometry \\iff f = g$$$

Lean4

@[simp]
theorem coe_toLinearIsometry : ⇑e.toLinearIsometry = e :=
  rfl

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

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

Разделы

Аффилиация

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