Commit 2023-08-31 10:55 dd94c82d

View on Github →

feat(Data/../ENNReal): add 2 lemmas (#6819)

Estimated changes

Modified Mathlib/Data/Real/ENNReal.lean

added theorem ENNReal.ofReal_lt_coe_iff

added theorem ENNReal.toReal_lt_of_lt_ofReal