Commit 2026-07-05 18:40 f682f8f0
View on Github →feat(Analysis/SpecialFunctions/Pow/Asymptotics): add Real.tendsto_rpow_atTop_of_base_gt_one (#41375)
Mathlib contains Real.tendsto_rpow_atTop_of_base_lt_one, Real.tendsto_rpow_atBot_of_base_lt_one, and Real.tendsto_rpow_atBot_of_base_gt_one, but Real.tendsto_rpow_atTop_of_base_gt_one was mysteriously missing. (For comparison, ENNReal has all four versions.) This PR fills in the gap by adding the fourth lemma (with a near-identical proof).