Commit 2025-02-10 05:14 1267df2e

View on Github →

refactor: restate lemmas about ∑' _, c using ENat.card/Set.encard (#21503) Previously, someone trying to simplify away ∑' _, c would stumble upon ENNReal.tsum_const_eq, turning the expression into c * count univ, and the only available rewrite from here would be count_apply turning the expression into c * ∑' _, 1! Also remove _eq from the relevant lemma names. From LeanAPAP

Estimated changes

Modified Mathlib/Data/Real/ENatENNReal.lean

added theorem ENat.toENNReal_eq_top

added theorem ENat.toENNReal_lt_top

added theorem ENat.toENNReal_ne_top

Modified Mathlib/MeasureTheory/Function/EssSup.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

modified theorem ENNReal.tsum_const_eq

Modified Mathlib/MeasureTheory/Measure/Count.lean

modified theorem MeasureTheory.Measure.count_apply

modified theorem MeasureTheory.Measure.count_apply_finset'

modified theorem MeasureTheory.Measure.count_empty

modified theorem MeasureTheory.Measure.count_univ

Modified Mathlib/Probability/UniformOn.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.mk_lt_aleph0

Modified Mathlib/SetTheory/Cardinal/ENat.lean

added theorem Cardinal.toENat_lt_top

added theorem Cardinal.toENat_ne_top

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem ENat.card_eq_top

added theorem ENat.card_lt_top_of_finite

Modified Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean

added theorem ENNReal.tsum_const

added theorem ENNReal.tsum_one

added theorem ENNReal.tsum_set_const

deleted theorem ENNReal.tsum_set_const_eq

added theorem ENNReal.tsum_set_one

deleted theorem ENNReal.tsum_set_one_eq