continuousAt_zpow — Mathlib

English

Continuity of the power map x ↦ x^n at x with condition x ≠ 0 or n ≥ 0.

Русский

Положение непрерывности отображения x ↦ x^n в точке x, если x ≠ 0 или n ≥ 0.

LaTeX

$$$\text{ContinuousAt}(x \mapsto x^{n}, x) \Leftrightarrow (x \neq 0) \lor (0 \le n).$$$

Lean4

@[simp]
protected theorem continuousAt_zpow : ContinuousAt (fun x ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n :=
  by
  refine ⟨?_, continuousAt_zpow₀ _ _⟩
  contrapose!
  rintro ⟨rfl, hm⟩ hc
  exact
    not_tendsto_atTop_of_tendsto_nhds (hc.tendsto.mono_left nhdsWithin_le_nhds).norm
      (NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop hm)

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