instZSMul — Mathlib

English

If β is an additive group with IsTopologicalAddGroup, then C(α,β) is a Z-module: there is an action of ℤ on C(α,β) given by (z • f)(x) = z • f(x).

Русский

Если β — аддитивная группа с IsTopologicalAddGroup, то множество непрерывных отображений C(α,β) является Z-модулем: действует действие ℤ на C(α,β) задаваемое (z • f)(x) = z • f(x).

LaTeX

$$$\forall z\in\mathbb{Z},\ \forall f:\ C(\alpha,\beta): (z\cdot f)(x) = z\cdot f(x) \quad\text{для всех } x. $$$

Lean4

instance instZSMul [AddGroup β] [IsTopologicalAddGroup β] : SMul ℤ C(α, β) where
  smul z f := ⟨z • ⇑f, f.continuous.zsmul z⟩

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