continuous_zpow — Mathlib

English

For every z ∈ ℤ, the map a ↦ a^z is continuous on G.

Русский

Для любого z ∈ ℤ отображение a ↦ a^z непрерывно на G.

LaTeX

$$$\forall z \in \mathbb{Z},\; a \mapsto a^{z} \text{ is continuous on } G.$$$

Lean4

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_zpow : ∀ z : ℤ, Continuous fun a : G => a ^ z
  | Int.ofNat n => by simpa using continuous_pow n
  | Int.negSucc n => by simpa using (continuous_pow (n + 1)).inv

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