Commit 2024-11-07 16:37 eba55e96

View on Github →

chore: generalise ENNReal lemmas to WithTop (#17786) That way, they will also apply to a potential future ENNRat.

Estimated changes

modified theorem Antitone.const_mul'
modified theorem Antitone.mul_const'
modified theorem AntitoneOn.mul_const'
modified theorem Monotone.const_mul'
modified theorem MonotoneOn.mul_const'
added theorem max_mul
added theorem mul_left_mono
added theorem mul_max
added theorem mul_right_mono
deleted theorem ENNReal.max_mul
deleted theorem ENNReal.mul_left_mono
modified theorem ENNReal.mul_lt_mul
deleted theorem ENNReal.mul_max
deleted theorem ENNReal.mul_right_mono
deleted theorem ENNReal.pow_strictMono