Commit 2026-03-10 15:17 3f7b757f

View on Github →

feat(Topology/Instances/EReal): limsup of multiplication by a constant (#35272) add an analogue of limsup_const_mul_of_ne_top which applies to EReal instead of ENNReal

Estimated changes

Modified Mathlib/Topology/Instances/EReal/Lemmas.lean

added theorem EReal.liminf_const_mul_of_nonneg_of_ne_top

added theorem EReal.liminf_const_mul_of_nonpos_of_ne_bot

added theorem EReal.limsup_const_mul_of_nonneg_of_ne_top

added theorem EReal.limsup_const_mul_of_nonpos_of_ne_bot