Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-09 22:52 e8758ae0

View on Github →

feat(measure_theory/*): a few lemmas about (is_)measurable in Π i, π i (#4948)

Estimated changes

Modified src/measure_theory/borel_space.lean

added theorem pi_le_borel_pi

Modified src/measure_theory/measurable_space.lean

added theorem is_measurable_pi

Modified src/measure_theory/measure_space.lean

deleted theorem measure_theory.measure_diff_of_ae_le