Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-10 09:40 6676917e

View on Github →

feat(analysis/special_functions/*): a few more simp lemmas (#4550) Add more lemmas for simplifying inequalities with exp, log, and rpow. Lemmas that generate more than one inequality are not marked as simp.

Estimated changes

modified theorem real.log_nonneg
added theorem real.log_nonneg_iff
added theorem real.log_nonpos_iff'
added theorem real.log_nonpos_iff
added theorem real.one_lt_rpow_iff
added theorem real.rpow_lt_one_iff
added theorem real.exp_le_one_iff
modified theorem real.exp_lt_one_iff
added theorem real.one_le_exp_iff
modified theorem real.one_lt_exp_iff