Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.rpow_add_le_add_rpow

Modification history

2022-08-04 15:03
src/analysis/mean_inequalities_pow.lean
chore(analysis/mean_inequalities_pow): weaken assumptions on rpow_add_le_rpow (#15823)
Modified nnreal.rpow_add_le_add_rpowView on Github →
2021-12-16 09:07
src/analysis/mean_inequalities_pow.lean
chore(analysis/mean_inequalities_pow): nnreal versions of some ennreal inequalities (#10836) …
Added nnreal.rpow_add_le_add_rpowView on Github →