compLinearMap — Mathlib

English

Composition with g is a linear map in the sense of C_c(γ, δ) →ₗ[R] C_c(β, δ) when δ is an AddCommMonoid with continuous addition and suitable module structure: toFun f = f ∘ g and map_add/map_smul hold.

Русский

Композиция через g образует линейное отображение в смысле C_c(γ, δ) →ₗ[R] C_c(β, δ) при δ – аддитивном коммутативном моноиде с непрерывным сложением и подходящей модульной структурой: toFun f = f ∘ g, а map_add/map_smul выполняются.

LaTeX

$$$$ (f + f') \circ g = f \circ g + f' \circ g, \quad (r \cdot f) \circ g = r \cdot (f \circ g). $$$$

Lean4

/-- Composition as a linear map. -/
def compLinearMap [AddCommMonoid δ] [ContinuousAdd δ] {R : Type*} [Semiring R] [Module R δ] [ContinuousConstSMul R δ]
    (g : β →co γ) : C_c(γ, δ) →ₗ[R] C_c(β, δ) where
  toFun f := f.comp g
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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