continuous_ofReal_cpow_const — Mathlib

English

For fixed y with Re(y) > 0, the map x ↦ (x : ℂ)^y is continuous in x.

Русский

Для фиксированного y с Re(y) > 0 отображение x ↦ (x : ℂ)^y непрерывно в x.

LaTeX

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

Lean4

theorem continuous_ofReal_cpow_const {y : ℂ} (hs : 0 < y.re) : Continuous (fun x => (x : ℂ) ^ y : ℝ → ℂ) :=
  continuous_iff_continuousAt.mpr fun x => continuousAt_ofReal_cpow_const x y (Or.inl hs)

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