coe_id

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The identity linear isometry has the same action as the identity map on the space.

Русский

Идентичная линейная изометрия действует как единичная карта на пространстве.

LaTeX

$$∀x, (id : E →ₗᵢ[R] E)(x) = x$$

Lean4

@[simp, norm_cast]
theorem coe_id : ((id : E →ₗᵢ[R] E) : E → E) = _root_.id :=
  rfl

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

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

Разделы

Аффилиация

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