Commit 2024-01-28 09:07 e8bfb678

View on Github →

refactor(Probability/Kernel/CondCdf): mv ofReal_cinfi (#10044)

Estimated changes

Modified Mathlib/Probability/Kernel/CondCdf.lean

deleted theorem ENNReal.ofReal_cinfi

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem ENNReal.ofReal_cinfi