Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-13 08:12
f697cccc
View on Github →
feat: lemmas about monotonicity and asymptotics of
rpow
(
#6140
)
Estimated changes
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
added
theorem
tendsto_rpow_atBot_of_base_gt_one
added
theorem
tendsto_rpow_atBot_of_base_lt_one
added
theorem
tendsto_rpow_atTop_of_base_gt_one
added
theorem
tendsto_rpow_atTop_of_base_lt_one
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
added
theorem
Real.antitone_rpow_of_base_le_one
added
theorem
Real.monotone_rpow_of_base_ge_one
added
theorem
Real.rpow_le_rpow_of_exponent_nonpos
added
theorem
Real.rpow_lt_rpow_of_exponent_neg
added
theorem
Real.strictAnti_rpow_of_base_lt_one
added
theorem
Real.strictMono_rpow_of_base_gt_one