Commit 2023-11-09 10:14 4dd5ba0b

View on Github →

chore(Data/Real/ENNReal): rename some to ofNNReal (#8276) The some name feels like an implementation detail.

Estimated changes

Modified Mathlib/Data/Real/ENNReal.lean

modified theorem ENNReal.coe_max

modified theorem ENNReal.coe_min

modified theorem ENNReal.coe_mono

modified theorem ENNReal.coe_strictMono

added def ENNReal.ofNNReal

modified theorem ENNReal.range_coe'

modified theorem ENNReal.range_coe

deleted def ENNReal.some

added def Mathlib.Meta.Positivity.evalENNRealOfNNReal

deleted def Mathlib.Meta.Positivity.evalENNRealSome

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/Probability/Variance.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean