Commit 2025-12-03 01:23 6920d300

View on Github →

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

Estimated changes

Modified Mathlib/Data/Finset/Pi.lean

modified theorem Finset.restrict_preimage

added theorem Finset.restrict_preimage_univ

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.pi_iUnion_eq_iInter_pi

Modified Mathlib/Order/CompleteLattice/Finset.lean

added theorem Set.iUnion_finset_eq_set

Modified Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

Modified Mathlib/Probability/ProductMeasure.lean

added theorem MeasureTheory.Measure.infinitePi_map_restrict'

added theorem MeasureTheory.Measure.infinitePi_pi_of_countable

added theorem MeasureTheory.Measure.infinitePi_pi_univ

modified theorem MeasureTheory.Measure.infinitePi_singleton

added theorem MeasureTheory.Measure.infinitePi_singleton_of_fintype

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

modified theorem tprod_singleton