Commit 2024-10-13 20:38 1e919af2

View on Github →

feat(Measure/Typeclasses): rename sFiniteSeq (#17423) Moves:

MeasureTheory.sFiniteSeq -> MeasureTheory.sfiniteSeq

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

deleted def MeasureTheory.sFiniteSeq

deleted theorem MeasureTheory.sFiniteSeq_le

deleted theorem MeasureTheory.sFiniteSeq_zero

added theorem MeasureTheory.sfiniteSeq_le

added theorem MeasureTheory.sfiniteSeq_zero

deleted theorem MeasureTheory.sum_sFiniteSeq

added theorem MeasureTheory.sum_sfiniteSeq

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

Modified Mathlib/MeasureTheory/Measure/WithDensityFinite.lean

deleted theorem MeasureTheory.sFiniteSeq_absolutelyContinuous_toFinite

added theorem MeasureTheory.sfiniteSeq_absolutelyContinuous_toFinite

Modified Mathlib/Probability/Kernel/Basic.lean