mathlib3

ba455ea6 - feat(special_functions/pow): continuity of real to complex power (#13244)

feat(special_functions/pow): continuity of real to complex power (#13244) Some lemmas excised from my Gamma-function project. The main result is that for a complex `s` with `re s > 0`, the function `(λ x, x ^ s : ℝ → ℂ)` is continuous on all of `ℝ`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>