Commit 2025-07-03 06:16 cac8b14c

View on Github →

feat: add iInf results on ENNReal, matching existing iSup ones (#26411)

Estimated changes

Modified Mathlib/Data/ENNReal/Operations.lean

added theorem ENNReal.add_iInf₂

added theorem ENNReal.add_sInf

added theorem ENNReal.exists_add_lt_of_add_lt

added theorem ENNReal.iInf_add_iInf_of_monotone

added theorem ENNReal.iInf_gt_eq_self

added theorem ENNReal.iInf₂_add

added theorem ENNReal.le_iInf_add_iInf

added theorem ENNReal.le_iInf₂_add_iInf₂