Theorem ENNReal.toReal_le_add'

Modification history

2026-10-28 12:53

Mathlib/Basic/ENNReal/Operations.lean

chore: rename `ENNReal.toReal_mono'` (#43856) …

Deleted ENNReal.toReal_le_add'View on Github →

2025-03-31 03:39

Mathlib/Data/ENNReal/Operations.lean

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

Modified ENNReal.toReal_le_add'View on Github →

2025-02-11 10:41

Mathlib/Data/ENNReal/Order.lean

chore(Data/ENNReal): restructure lemma files (#21649) …

Modified ENNReal.toReal_le_add'View on Github →

2024-01-25 21:01

Mathlib/Data/ENNReal/Basic.lean

chore(Data/ENNReal/Basic): split file (#9869)

Modified ENNReal.toReal_le_add'View on Github →

2023-04-07 13:27

Mathlib/Data/Real/ENNReal.lean

feat: port Topology.MetricSpace.HausdorffDistance (#3313)

Added ENNReal.toReal_le_add'View on Github →