continuousAt_const_rpow — Mathlib

English

For a ≠ 0, the map a^· as a function of the exponent is continuous (Real version).

Русский

Для a ≠ 0 отображение x ↦ a^x непрерывно по x в вещественном случае.

LaTeX

$$$$\\forall a\\in \\mathbb{R},\\ a\\neq 0\\;\\Rightarrow\\; \\text{ContinuousAt}(x \\mapsto a^{x}, b). $$$$

Lean4

theorem continuousAt_const_rpow {a b : ℝ} (h : a ≠ 0) : ContinuousAt (a ^ ·) b :=
  by
  simp only [rpow_def]
  refine Complex.continuous_re.continuousAt.comp ?_
  refine (continuousAt_const_cpow ?_).comp Complex.continuous_ofReal.continuousAt
  norm_cast

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