English
As an instance, if A is an AddMonoid with a topology making addition continuous, then the natural-number smul action ℕ × A → A is continuous.
Русский
Как пример, если A — добавочное моноид с топологией, при которой сложение непрерывно, тогда отображение ℕ × A → A, (n,a) ↦ n·a, непрерывно.
LaTeX
$$$\\text{ContinuousSMul }\\mathbb{N} A$$$
Lean4
instance continuousSMul_nat {A} [AddMonoid A] [TopologicalSpace A] [ContinuousAdd A] : ContinuousSMul ℕ A :=
⟨continuous_prod_of_discrete_left.mpr continuous_nsmul⟩
-- We register `Continuous.pow` as a `continuity` lemma with low penalty (so
-- `continuity` will try it before other `continuity` lemmas). This is a
-- workaround for goals of the form `Continuous fun x => x ^ 2`, where
-- `continuity` applies `Continuous.mul` since the goal is defeq to
-- `Continuous fun x => x * x`.
--
-- To properly fix this, we should make sure that `continuity` applies its
-- lemmas with reducible transparency, preventing the unfolding of `^`. But this
-- is quite an invasive change.
