Commit 2025-03-06 13:50 4954b32d

feat(Analysis/SpecialFunctions/Pow): add continuity of constant^x for real x (#22588) Add the lemma continuous_const_rpow Motivation: There is lemma continuous_const_cpow to prove constant^x is continuous for complex x, but no analogue lemma for real exists. This also causes difficulty to prove such facts using fun_prop. See minor discussion on Zulip.