Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-10 16:03 021c8590

View on Github →

feat(analysis/special_functions/pow): rpow-log inequalities (#7848) Inequalities relating rpow and log

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem real.le_rpow_iff_log_le

added theorem real.le_rpow_of_log_le

added theorem real.lt_rpow_iff_log_lt

added theorem real.lt_rpow_of_log_lt