Commit 2024-01-08 08:22 03bf7743

View on Github →

chore(*): use ∞ for ⊤ : ENNReal (#9541)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.measure_liminf_eq_zero

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

modified theorem ENNReal.continuous_sub_left

modified theorem ENNReal.iInf_mul_left'

modified theorem ENNReal.iInf_mul_right'

modified theorem ENNReal.isOpen_ne_top

modified theorem ENNReal.nhds_of_ne_top

modified theorem ENNReal.sub_iSup

modified theorem ENNReal.tendsto_toNNReal

modified theorem ENNReal.tendsto_toReal

modified theorem ENNReal.tsum_lt_tsum

modified theorem Summable.countable_support_ennreal

modified theorem continuous_of_le_add_edist

modified theorem edist_ne_top_of_mem_ball