Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-03 11:59 0837fc30

View on Github →

feat(measure_theory/pi): finite products of measures (#5414) See module doc of measure_theory/pi.lean

Estimated changes

Modified src/measure_theory/measurable_space.lean

added theorem is_measurable.tprod

added theorem measurable_tprod_elim'

added theorem measurable_tprod_elim

added theorem measurable_tprod_mk

Created src/measure_theory/pi.lean

added def measure_theory.measure.pi'

added theorem measure_theory.measure.pi'_pi

added theorem measure_theory.measure.pi'_pi_le

added theorem measure_theory.measure.pi_caratheodory

added theorem measure_theory.measure.pi_pi

added theorem measure_theory.measure.tprod_cons

added theorem measure_theory.measure.tprod_nil

added theorem measure_theory.measure.tprod_tprod

added theorem measure_theory.measure.tprod_tprod_le

added theorem measure_theory.outer_measure.le_pi

added theorem measure_theory.outer_measure.pi_pi_le

added def measure_theory.pi_premeasure

added theorem measure_theory.pi_premeasure_pi'

added theorem measure_theory.pi_premeasure_pi

added theorem measure_theory.pi_premeasure_pi_eval

added theorem measure_theory.pi_premeasure_pi_mono