Theorem MeasureTheory.sFiniteSeq_le

Modification history

2024-10-13 20:38

Mathlib/MeasureTheory/Measure/Typeclasses.lean

feat(Measure/Typeclasses): rename `sFiniteSeq` (#17423) …

Deleted MeasureTheory.sFiniteSeq_le View on Github →

2024-10-11 13:11

Mathlib/MeasureTheory/Measure/Typeclasses.lean

feat(Measure/WithDensityFinite): redefine `Measure.toFinite` (#17421) …

Added MeasureTheory.sFiniteSeq_le View on Github →