log): Relating `log`-inequalities and `exp`-inequalities (#10191)

Commit

4 years ago

feat(analysis/special_functions/log): Relating `log`-inequalities and `exp`-inequalities (#10191) This proves `log x ≤ y ↔ x ≤ exp y` and `x ≤ log y ↔ exp x ≤ y`.

Author

YaelDillies

Parents

169bb29d

mathlib daac8545 - feat(analysis/special_functions/log): Relating `log`-inequalities and `exp`-inequalities (#10191)

mathlib
daac8545 - feat(analysis/special_functions/log): Relating `log`-inequalities and `exp`-inequalities (#10191)