continuous_pow — Mathlib

English

In a topological monoid M with continuous multiplication, for every natural number n, the map a ↦ a^n is continuous.

Русский

В топологическом моноиде M с непрерывным умножением для каждого натурального числа n отображение a ↦ a^n непрерывно.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; \\text{Continuous}(a \\mapsto a^n)$$$

Lean4

@[to_additive (attr := continuity)]
theorem continuous_pow : ∀ n : ℕ, Continuous fun a : M => a ^ n
  | 0 => by simpa using continuous_const
  | k + 1 => by
    simp only [pow_succ']
    exact continuous_id.mul (continuous_pow _)

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