zero_cpow_eq_nhds — Mathlib

English

If b ≠ 0, then near b the function x ↦ 0^x is identically 0; i.e., 0^x tends to 0 as x approaches b.

Русский

Пусть b ≠ 0. Тогда в окрестности b функция x ↦ 0^x тождественно равна 0; то есть 0^x стремится к 0 при x → b.

LaTeX

$$$$\\text{If } b \\neq 0,\\quad (0)^{x} = 0 \\text{ for } x \\text{ in a neighborhood of } b.$$$$

Lean4

theorem zero_cpow_eq_nhds {b : ℂ} (hb : b ≠ 0) : (fun x : ℂ => (0 : ℂ) ^ x) =ᶠ[𝓝 b] 0 :=
  by
  suffices ∀ᶠ x : ℂ in 𝓝 b, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [zero_cpow hx, Pi.zero_apply]
  exact IsOpen.eventually_mem isOpen_ne hb

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