Theorem MeasureTheory.Measure.isFiniteMeasure_map_iff

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_map_iff View on Github →