Commit 2025-10-28 13:23 16f65d87

View on Github →

feat(ENNReal): equality from comparing with nnreals (#30721) And rename the existing lemma as it is ambiguous.

Estimated changes

Modified Mathlib/Data/ENNReal/Inv.lean

added theorem ENNReal.eq_of_forall_le_nnreal_iff

deleted theorem ENNReal.eq_of_forall_nnreal_iff

added theorem ENNReal.eq_of_forall_nnreal_le_iff

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.eq_of_forall_coe_le_iff

added theorem WithBot.forall_coe_le_iff_le

added theorem WithTop.eq_of_forall_le_coe_iff

added theorem WithTop.forall_le_coe_iff_le

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