compMulHom — Mathlib

English

Composition with g defines a multiplicative monoid homomorphism from the cocompact maps to cocompact maps: (f1 f2) ∘ g = (f1 ∘ g)(f2 ∘ g).

Русский

Композиция через g задаёт умножающим гомоморфизм из CocompactMap β γ в CocompactMap β δ: (f1 f2) ∘ g = (f1 ∘ g)(f2 ∘ g).

LaTeX

$$$$ (f_1 f_2) \circ g = (f_1 \circ g)(f_2 \circ g). $$$$

Lean4

/-- Composition as a semigroup homomorphism. -/
def compMulHom [MulZeroClass δ] [ContinuousMul δ] (g : β →co γ) : C_c(γ, δ) →ₙ* C_c(β, δ)
    where
  toFun f := f.comp g
  map_mul' _ _ := rfl

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