comp — Mathlib

English

For a finite index set and a family of endomorphisms, the finite sum of endomorphisms composes with a map f as the finite sum of compositions: (∑ f_i) ∘ f = ∑ (f_i ∘ f).

Русский

Для конечного множителя индексов и семьи эндоморфизмов итоговая сумма компонуется с отображением f так же, как и по элементам: (∑ f_i) ∘ f = ∑ (f_i ∘ f).

LaTeX

$$$\\left(\\sum_{i\\in s} f_i\\right) \\circ f = \\sum_{i\\in s} (f_i \\circ f).$$$

Lean4

/-- Composition of bounded linear maps. -/
def comp (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : M₁ →SL[σ₁₃] M₃ :=
  ⟨(g : M₂ →ₛₗ[σ₂₃] M₃).comp (f : M₁ →ₛₗ[σ₁₂] M₂), g.2.comp f.2⟩

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