Continuity of power functions #
This file contains lemmas about continuity of the power functions on
Continuity for complex powers #
z ^ w is continuous in
(z, w) provided that
z does not belong to the interval
(-∞, 0] on the real line. See also
Complex.continuousAt_cpow_zero_of_re_pos for a version that
z = 0 but assumes
0 < re w.
Continuity for real powers #
These results involve relating real and complex powers, so cannot be done higher up.