Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-13 14:54 c8574c89

View on Github →

feat(analysis/special_functions/pow): add various lemmas about ennreal.rpow (#5701)

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem ennreal.le_rpow_one_div_iff

added theorem ennreal.lt_rpow_one_div_iff

added theorem ennreal.rpow_eq_top_iff_of_pos

added theorem ennreal.rpow_le_rpow_iff

added theorem ennreal.rpow_left_bijective

added theorem ennreal.rpow_left_injective

added theorem ennreal.rpow_left_monotone_of_nonneg

added theorem ennreal.rpow_left_strict_mono_of_pos

added theorem ennreal.rpow_left_surjective

added theorem ennreal.rpow_lt_rpow_iff

added theorem ennreal.rpow_pos

added theorem ennreal.rpow_pos_of_nonneg