coe_trans

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

For e1: E→E2 and e2: E2→E3, the action of the composed equivalence on an input c is e2(e1(c)).

Русский

Для e1 и e2 соответствующий композиции эквивалент применим к входу c как e2(e1(c)).

LaTeX

$$$ (e_1 \\trans e_2)(c) = e_2(e_1(c)) $$$

Lean4

@[simp]
theorem coe_trans (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ :=
  rfl

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

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

Разделы

Аффилиация

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