Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-04 15:03 7eaf3412

View on Github →

chore(analysis/mean_inequalities_pow): weaken assumptions on rpow_add_le_rpow (#15823)

Estimated changes

Modified src/analysis/mean_inequalities_pow.lean

modified theorem ennreal.rpow_add_le_add_rpow

modified theorem nnreal.rpow_add_le_add_rpow

Modified src/analysis/normed_space/lp_space.lean

Modified src/measure_theory/function/lp_space.lean