Commit 2024-11-20 08:25 23f454fb
View on Github →refactor(EReal): add add/sub lemmas and refactor limsup_add on EReal (#18879) This PR :
- adds a few lemmas about addition/subtraction in
Topology.Instances.EReal. These are translations inERealof similar lemmas about multiplication/division inENNReal(seeData.ENNReal.Inv). - renames EReal.add_le_of_forall_add_le, EReal.le_add_of_forall_le_add to bring them in line with similar lemmas in
Real/ENNReal(see e.g. add_le_of_forall_lt) - simplifies significantly the proofs of
add_le_of_forall_ltandle_add_of_forall_lt. - renames EReal.add_liminf_le_liminf_add, EReal.limsup_add_le_add_limsup, EReal.limsup_add_liminf_le_limsup_add, EReal.liminf_add_le_limsup_add_liminf to bring them in line with similar lemmas in
Real/ENNReal(see e.g. ENNReal.limsup_mul_le) - removes EReal.le_of_forall_lt_iff_le, EReal.ge_of_forall_gt_iff_ge, EReal.limsup_le_iff which were very specialized lemmas used only in the older version of the proofs above.