continuousAt_zpow₀ — Mathlib

English

If a ∈ G₀ and m ∈ ℤ, then x ↦ x^m is continuous at a provided a ≠ 0 or m ≥ 0.

Русский

Пусть a ∈ G₀ и m ∈ ℤ; функция x ↦ x^m непрерывна в точке a при условии a ≠ 0 или m ≥ 0.

LaTeX

$$$\\text{ContinuousAt}(x \\mapsto x^{m})\\ a, \\quad \\text{при } (a \\neq 0 \\lor 0 \\le m)$$$

Lean4

theorem continuousAt_zpow₀ (x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) : ContinuousAt (fun x => x ^ m) x :=
  by
  rcases m with m | m
  · simpa only [Int.ofNat_eq_coe, zpow_natCast] using continuousAt_pow x m
  · simp only [zpow_negSucc]
    have hx : x ≠ 0 := h.resolve_right (Int.negSucc_lt_zero m).not_ge
    exact (continuousAt_pow x (m + 1)).inv₀ (pow_ne_zero _ hx)

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