Commit 2025-03-07 17:17 7b4a09d2

View on Github →

feat: ENNReal.ofNNReal preserves limsup and liminf (#22659)

Estimated changes

Modified Mathlib/Data/ENNReal/Inv.lean

added theorem ENNReal.eq_of_forall_nnreal_iff

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

modified theorem ENNReal.le_liminf_mul

modified theorem ENNReal.le_limsup_mul

modified theorem ENNReal.liminf_mul_le

modified theorem ENNReal.liminf_toReal_eq

modified theorem ENNReal.limsup_mul_le'

modified theorem ENNReal.limsup_toReal_eq

added theorem ENNReal.ofNNReal_liminf

added theorem ENNReal.ofNNReal_limsup