add_comp — Mathlib

English

Distributivity of composition over addition: (h+g) ∘ f = h ∘ f + g ∘ f for linear maps f: M →ₛₗ[σ₁₂] M₂, g,h: M₂ →ₛₗ[σ₂₃] M₃.

Русский

Расслоение по сложению сохраняется: (h+g) ∘ f = h ∘ f + g ∘ f для линейных отображений.

LaTeX

$$$(f : M \to_{\sigma_{12}} M_2)(g,h : M_2 \to_{\sigma_{23}} M_3) \,:\; (h+g) \circ f = h \circ f + g \circ f$$$

Lean4

theorem add_comp (f : M →ₛₗ[σ₁₂] M₂) (g h : M₂ →ₛₗ[σ₂₃] M₃) : ((h + g).comp f : M →ₛₗ[σ₁₃] M₃) = h.comp f + g.comp f :=
  rfl

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