Commit 2025-02-22 09:01 f9d83939

View on Github →

feat(Topology/Instances/EReal/Lemmas): add lemmas about limsup and multiplication (#21833) This PR adds lemmas about liminf (u * v) and limsup (u * v) in extended reals. See this file for similar results in the reals. The strategy is the same, with a bunch of auxiliary lemmas in Data/Real/EReal. I also took this opportunity to do some moderate cleaning in Data/Real/EReal: minor golfing and uniformization of variable names.

Estimated changes

modified theorem EReal.div_eq_iff
modified theorem EReal.div_le_iff_le_mul
modified theorem EReal.div_lt_iff
modified theorem EReal.div_mul_cancel
added theorem EReal.div_mul_div_comm
modified theorem EReal.div_nonneg
added theorem EReal.div_pos
modified theorem EReal.le_div_iff_mul_le
modified theorem EReal.lt_div_iff
modified theorem EReal.mul_div_cancel
modified theorem EReal.mul_div_mul_cancel
modified theorem EReal.mul_div_right
added theorem EReal.le_liminf_mul
added theorem EReal.le_limsup_mul
modified theorem EReal.liminf_add_gt_of_gt
added theorem EReal.liminf_mul_le
modified theorem EReal.limsup_add_le_of_le
added theorem EReal.limsup_mul_le