id

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The underlying function of the composition of two linear isometries equals the composition of their underlying functions.

Русский

Базовая функция композиции двух линейных изометрий равна композиции их базовых функций.

LaTeX

$$⇑(g.comp f) = g ∘ f$$

Lean4

/-- The identity linear isometry. -/
def id : E →ₗᵢ[R] E :=
  ⟨LinearMap.id, fun _ => rfl⟩

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

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

Разделы

Аффилиация

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