Commit 2020-09-08 21:33 f5ee84c9

View on Github →

feat(analysis/special_functions/pow): Added lemmas bounding rpow in ennreal (#4039) Continuation of #3715. Added lemmas in ennreal corresponding to the real and nnreal lemmas added in that PR

Estimated changes

Modified src/analysis/special_functions/pow.lean

modified theorem ennreal.one_le_rpow

added theorem ennreal.one_le_rpow_of_pos_of_le_one_of_neg

added theorem ennreal.one_lt_rpow_of_pos_of_lt_one_of_neg

modified theorem ennreal.rpow_le_one

added theorem ennreal.rpow_le_one_of_one_le_of_neg

modified theorem ennreal.rpow_lt_one

added theorem ennreal.rpow_lt_one_of_one_lt_of_neg