continuousConstSMul_nat — Mathlib

English

If A is an AddMonoid with a topology making addition continuous, then the natural-number scalar action ℕ × A → A, (n,a) ↦ n·a, is continuous.

Русский

Пусть A — добавочное моноид с топологией, при которой сложение непрерывно; тогда отображение ℕ × A → A, (n,a) ↦ n·a, непрерывно.

LaTeX

$$$\\text{ContinuousConstSMul }\\mathbb{N} A$$$

Lean4

instance continuousConstSMul_nat {A} [AddMonoid A] [TopologicalSpace A] [ContinuousAdd A] : ContinuousConstSMul ℕ A :=
  ⟨continuous_nsmul⟩

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