continuousConstSMul_int — Mathlib

English

The integer scalar action on an additive group A is continuous; i.e., n ↦ n • a is continuous in a for fixed integer n.

Русский

Целочисленное действие на аддитивной группе A непрерывно: для фиксированного n отображение a ↦ n • a непрерывно в a.

LaTeX

$$$\text{ContinuousConstSMul } \mathbb{Z} A.$$$

Lean4

instance continuousConstSMul_int {A} [AddGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] :
    ContinuousConstSMul ℤ A :=
  ⟨continuous_zsmul⟩

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