Theorem EReal.le_add_of_forall_gt

Modification history

2025-03-31 03:39

Mathlib/Data/EReal/Basic.lean

chore: split `Data.EReal.Basic` (#23428) …

Modified EReal.le_add_of_forall_gt View on Github →

2024-11-20 08:25

Mathlib/Data/Real/EReal.lean

refactor(EReal): add add/sub lemmas and refactor limsup_add on EReal (#18879) …

Added EReal.le_add_of_forall_gt View on Github →