Commit 2024-02-06 07:47 e2cf2aef

View on Github →

chore(MeasureTheory): Fintype -> Finite (#10289)

Rename hasFiniteIntegral_of_fintype to HasFiniteIntegral.of_finite, generalize to [Finite α], golf.
Rename integrable_of_fintype to Integrable.of_finite, generalize to [Finite α].
Rename SimpleFunc.ofFintype to SimpleFunc.ofFinite, generalize to [Finite α], use it to golf SimpleFunc.ofIsEmpty.
Rename stronglyMeasurable_of_fintype to StronglyMeasurable.of_finite, deprecate stronglyMeasurable_of_isEmpty.

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.HasFiniteIntegral.of_finite

added theorem MeasureTheory.Integrable.of_finite

deleted theorem MeasureTheory.hasFiniteIntegral_of_fintype

deleted theorem MeasureTheory.integrable_of_fintype

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

added def MeasureTheory.SimpleFunc.ofFinite

deleted def MeasureTheory.SimpleFunc.ofFintype

modified def MeasureTheory.SimpleFunc.ofIsEmpty

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

added theorem MeasureTheory.StronglyMeasurable.of_finite

deleted theorem MeasureTheory.stronglyMeasurable_of_fintype

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Integrals.lean