Commit 2024-08-29 16:54 37864dde

View on Github →

feat(EReal): rework limsup_add properties (#15261) Rework of properties about iSup/iInf/limsup/liminf and addition in extended reals:

A key property about addition and order has been abstracted away in Data.Real.Ereal. Three new lemmas add_le_of_forall_lt_add_top, add_le_of_forall_lt_add, le_add_of_forall_gt_add. The first one is private (generalized by the second one).
These new lemmas allow for very streamlined proofs of add_liminf_le_liminf_add and limsup_add_le_add_limsup in Topology.instances.EReal. I've also deleted a few intermediate lemmas which are not needed anymore.
These new lemmas also allow for short proofs of a few more useful lemmas: add_iInf_le_iInf_add, iSup_add_le_add_iSup about Inf/Sup, and limsup_add_liminf_le_limsup_add, liminf_add_le_limsup_add_liminf about limsup/liminf.

Estimated changes

Modified Mathlib/Data/Real/EReal.lean

added theorem EReal.add_le_of_forall_add_le

deleted theorem EReal.ge_iff_le_forall_real_lt

added theorem EReal.ge_of_forall_gt_iff_ge

added theorem EReal.le_add_of_forall_le_add

deleted theorem EReal.le_iff_le_forall_real_gt

added theorem EReal.le_of_forall_lt_iff_le

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.forall_le_iff_eq_bot

added theorem WithBot.ge_of_forall_gt_iff_ge

added theorem WithBot.le_of_forall_lt_iff_le

added theorem WithTop.forall_ge_iff_eq_top

added theorem WithTop.forall_gt_iff_eq_top

deleted theorem WithTop.forall_lt_iff_eq_top

added theorem WithTop.ge_of_forall_gt_iff_ge

added theorem WithTop.le_of_forall_lt_iff_le

Modified Mathlib/Topology/Instances/EReal.lean

added theorem EReal.add_iInf_le_iInf_add

added theorem EReal.iSup_add_le_add_iSup

added theorem EReal.liminf_add_le_limsup_add_liminf

deleted theorem EReal.liminf_le_liminf

modified theorem EReal.limsup_add_le_add_limsup

added theorem EReal.limsup_add_liminf_le_limsup_add

deleted theorem EReal.limsup_add_lt_of_lt

deleted theorem EReal.limsup_le_limsup