continuousAt_cpow_const_of_re_pos

English

For p = (z,w) with Re(z) ≥ 0 or Im(z) ≠ 0 and Re(w) > 0, the map x ↦ x^w is continuous at z.

Русский

Для p=(z,w) с (Re(z) ≥ 0 или Im(z) ≠ 0) и Re(w) > 0 отображение x ↦ x^w непрерывно в z.

LaTeX

$$$$\forall p=(z,w),\ (\Re(z) \ge 0 \lor \Im(z) \neq 0) \land \Re(w) > 0 \Rightarrow \text{ContinuousAt}(x\mapsto x^w)\, z.$$$$

Lean4

/-- See also `continuousAt_cpow_const` for a version that assumes `z ≠ 0` but makes no
assumptions about `w`. -/
theorem continuousAt_cpow_const_of_re_pos {z w : ℂ} (hz : 0 ≤ re z ∨ im z ≠ 0) (hw : 0 < re w) :
    ContinuousAt (fun x => x ^ w) z :=
  Tendsto.comp (@continuousAt_cpow_of_re_pos (z, w) hz hw) (continuousAt_id.prodMk continuousAt_const)

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