Theorem ENNReal.range_coe'

Modification history

2023-11-09 10:14

Mathlib/Data/Real/ENNReal.lean

chore(Data/Real/ENNReal): rename `some` to `ofNNReal` (#8276) …

Modified ENNReal.range_coe'View on Github →

2023-03-14 07:09

Mathlib/Data/Real/ENNReal.lean

feat: port Topology.Instances.Ereal (#2796) …

Added ENNReal.range_coe'View on Github →