Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-11 21:22 049f16a8

View on Github →

feat(measure_theory/pi): ae_eq lemmas about intervals in Π i, α i (#5633)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.pi_inter_distrib

Modified src/data/set/lattice.lean

modified theorem set.pi_def

added theorem set.pi_diff_pi_subset

Modified src/measure_theory/measurable_space.lean

Modified src/measure_theory/pi.lean

added theorem measure_theory.measure.ae_eq_pi

added theorem measure_theory.measure.ae_eq_set_pi

added theorem measure_theory.measure.ae_eval_ne

added theorem measure_theory.measure.ae_le_pi

added theorem measure_theory.measure.ae_le_set_pi

added theorem measure_theory.measure.ae_pi_le_infi_comap

added theorem measure_theory.measure.pi_Ico_ae_eq_pi_Icc

added theorem measure_theory.measure.pi_Iio_ae_eq_pi_Iic

added theorem measure_theory.measure.pi_Ioc_ae_eq_pi_Icc

added theorem measure_theory.measure.pi_Ioi_ae_eq_pi_Ici

added theorem measure_theory.measure.pi_Ioo_ae_eq_pi_Icc

modified theorem measure_theory.measure.pi_eval_preimage_null

added theorem measure_theory.measure.pi_has_no_atoms

modified theorem measure_theory.measure.pi_hyperplane

modified theorem measure_theory.measure.pi_pi

added theorem measure_theory.measure.tendsto_eval_ae_ae

added theorem measure_theory.measure.univ_pi_Ico_ae_eq_Icc

added theorem measure_theory.measure.univ_pi_Iio_ae_eq_Iic

added theorem measure_theory.measure.univ_pi_Ioc_ae_eq_Icc

added theorem measure_theory.measure.univ_pi_Ioi_ae_eq_Ici

added theorem measure_theory.measure.univ_pi_Ioo_ae_eq_Icc