instSMulInt — Mathlib

English

There is a natural ℤ-module structure on the space of bounded continuous maps α →ᵇ β, i.e., integer scaling is defined and respects boundedness and continuity.

Русский

Пространство ограниченных непрерывных отображений обладает структурой модуля над ℤ: целочисленное умножение определено и сохраняет ограниченность и непрерывность.

LaTeX

$$$\text{SMul}_{\mathbb{Z}}:\mathbb{Z} \times (\alpha \to^b \beta) \to (\alpha \to^b \beta)$$$

Lean4

instance instSMulInt : SMul ℤ (α →ᵇ β) where
  smul n
    f :=
    { toContinuousMap := n • f.toContinuousMap
      map_bounded' := by simpa using (zsmulRec (· • ·) n f).map_bounded' }

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