Theorem ENNReal.le_sub_iff_add_le_left

Modification history

2025-07-14 12:58
Mathlib/Data/ENNReal/Operations.lean
feat(Data/ENNReal): Add `sub_lt_iff_lt_left` and similar lemmas (#26815) …
Added ENNReal.le_sub_iff_add_le_leftView on Github →