continuousAt_ofReal_cpow_const — Mathlib

English

If y ∈ ℂ with Re(y) > 0, then x ↦ (x : ℂ)^y is continuous as a function of x on ℝ.

Русский

Если y ∈ ℂ и Re(y) > 0, тогда x ↦ (x : ℂ)^y непрерывно в x на ℝ.

LaTeX

$$$$\forall y\in\mathbb{C},\ \operatorname{Re}(y) > 0 \Rightarrow \text{ContinuousAt}(x\mapsto (x\,\text{as }\mathbb{C})^y)\text{ for } x\in\mathbb{R}.$$$$

Lean4

theorem continuousAt_ofReal_cpow_const (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
    ContinuousAt (fun a => (a : ℂ) ^ y : ℝ → ℂ) x :=
  (continuousAt_ofReal_cpow x y h).comp₂_of_eq (by fun_prop) (by fun_prop) rfl

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