Commit 2025-01-13 10:36 ff8b24e8

View on Github →

feat(EReal): add toENNReal (#18885)

Add definition of EReal.toENNReal.
Add some API lemmas for toENNReal.
Add measurability and continuity lemmas for toENNReal.

Estimated changes

Modified Mathlib/Data/Real/EReal.lean

added theorem EReal.add_ne_top_iff_of_ne_bot

added theorem EReal.add_ne_top_iff_of_ne_bot_of_ne_top

added theorem EReal.coe_toENNReal

added theorem EReal.coe_toENNReal_eq_max

added theorem EReal.real_coe_toENNReal

added theorem EReal.toENNReal_add

added theorem EReal.toENNReal_add_le

added theorem EReal.toENNReal_bot

added theorem EReal.toENNReal_coe

added theorem EReal.toENNReal_eq_toENNReal

added theorem EReal.toENNReal_eq_top_iff

added theorem EReal.toENNReal_eq_zero_iff

added theorem EReal.toENNReal_le_toENNReal

added theorem EReal.toENNReal_lt_toENNReal

added theorem EReal.toENNReal_mul'

added theorem EReal.toENNReal_mul

added theorem EReal.toENNReal_ne_top_iff

added theorem EReal.toENNReal_ne_zero_iff

added theorem EReal.toENNReal_of_ne_top

added theorem EReal.toENNReal_of_nonpos

added theorem EReal.toENNReal_sub

added theorem EReal.toENNReal_top

added theorem EReal.toENNReal_zero

added theorem EReal.toReal_toENNReal

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

added theorem AEMeasurable.ereal_toENNReal

added theorem Measurable.ereal_toENNReal

added theorem measurable_ereal_toENNReal

Modified Mathlib/Topology/Instances/EReal.lean

added theorem Continous.ereal_toENNReal

added theorem ContinuousAt.ereal_toENNReal

added theorem ContinuousOn.ereal_toENNReal

added theorem ContinuousWithinAt.ereal_toENNReal

added theorem EReal.continuous_toENNReal