instCommGroupContinuousMap — Mathlib

English

Right composition by a continuous map g: C(α, β) → C(β, γ) yields a MonoidHom from C(β, γ) to C(α, γ).

Русский

Правая композиция непрерывного отображения даёт моноидгомоморфизм между C(β, γ) и C(α, γ).

LaTeX

$$$\forall g:\, C(\alpha, \beta)\to C(\beta, \gamma),\; f\mapsto f\circ g$$$

Lean4

@[to_additive]
instance instCommGroupContinuousMap [CommGroup β] [IsTopologicalGroup β] : CommGroup C(α, β) :=
  coe_injective.commGroup _ coe_one coe_mul coe_inv coe_div coe_pow coe_zpow

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