Theorem MeasureTheory.stronglyMeasurable_of_fintype

Modification history

2024-02-06 07:47
Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
chore(MeasureTheory): `Fintype` -> `Finite` (#10289) …
Deleted MeasureTheory.stronglyMeasurable_of_fintypeView on Github →
2023-09-15 18:54
Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
feat: Pmf.integral_eq_sum (#6454) …
Added MeasureTheory.stronglyMeasurable_of_fintypeView on Github →