Theorem MeasureTheory.Measure.infinitePi_map_restrict'

Modification history

2025-12-03 01:23

Mathlib/Probability/ProductMeasure.lean

feat(Probability): version of `infinitePi_pi` for countable sets (#32287)

Added MeasureTheory.Measure.infinitePi_map_restrict'View on Github →