Theorem MeasureTheory.Measure.isFiniteMeasure_of_map

Modification history

2025-09-26 11:33

Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean

feat(MeasureTheory/ProbabilityTheory): `Is(Probability/Finite)Measure` iff map `Is(Probability/Finite)Measure` (#29922) …

Added MeasureTheory.Measure.isFiniteMeasure_of_map View on Github →