Commit 2023-06-01 03:52 785b8255

View on Github →

feat: port MeasureTheory.Constructions.Pi (#4501)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/Pi.lean

added theorem IsCountablySpanning.pi

added theorem IsPiSystem.pi

added def MeasureTheory.Measure.FiniteSpanningSetsIn.pi

added theorem MeasureTheory.Measure.ae_eq_pi

added theorem MeasureTheory.Measure.ae_eq_set_pi

added theorem MeasureTheory.Measure.ae_eval_ne

added theorem MeasureTheory.Measure.ae_le_pi

added theorem MeasureTheory.Measure.ae_le_set_pi

added theorem MeasureTheory.Measure.ae_pi_le_pi

added def MeasureTheory.Measure.pi'

added theorem MeasureTheory.Measure.pi'_eq_pi

added theorem MeasureTheory.Measure.pi'_pi

added theorem MeasureTheory.Measure.pi_Ico_ae_eq_pi_Icc

added theorem MeasureTheory.Measure.pi_Iio_ae_eq_pi_Iic

added theorem MeasureTheory.Measure.pi_Ioc_ae_eq_pi_Icc

added theorem MeasureTheory.Measure.pi_Ioi_ae_eq_pi_Ici

added theorem MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Icc

added theorem MeasureTheory.Measure.pi_Ioo_ae_eq_pi_Ioc

added theorem MeasureTheory.Measure.pi_ball

added theorem MeasureTheory.Measure.pi_caratheodory

added theorem MeasureTheory.Measure.pi_closedBall

added theorem MeasureTheory.Measure.pi_eq

added theorem MeasureTheory.Measure.pi_eq_generateFrom

added theorem MeasureTheory.Measure.pi_eval_preimage_null

added theorem MeasureTheory.Measure.pi_hyperplane

added theorem MeasureTheory.Measure.pi_noAtoms

added theorem MeasureTheory.Measure.pi_of_empty

added theorem MeasureTheory.Measure.pi_pi

added theorem MeasureTheory.Measure.pi_pi_aux

added theorem MeasureTheory.Measure.tendsto_eval_ae_ae

added theorem MeasureTheory.Measure.tprod_cons

added theorem MeasureTheory.Measure.tprod_nil

added theorem MeasureTheory.Measure.tprod_tprod

added theorem MeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc

added theorem MeasureTheory.Measure.univ_pi_Iio_ae_eq_Iic

added theorem MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc

added theorem MeasureTheory.Measure.univ_pi_Ioi_ae_eq_Ici

added theorem MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc

added theorem MeasureTheory.OuterMeasure.le_pi

added theorem MeasureTheory.OuterMeasure.pi_pi_le

added theorem MeasureTheory.measurePreserving_finTwoArrow

added theorem MeasureTheory.measurePreserving_finTwoArrow_vec

added theorem MeasureTheory.measurePreserving_funUnique

added theorem MeasureTheory.measurePreserving_piEquivPiSubtypeProd

added theorem MeasureTheory.measurePreserving_piFinSuccAboveEquiv

added theorem MeasureTheory.measurePreserving_piFinTwo

added theorem MeasureTheory.measurePreserving_pi_empty

added def MeasureTheory.piPremeasure

added theorem MeasureTheory.piPremeasure_pi'

added theorem MeasureTheory.piPremeasure_pi

added theorem MeasureTheory.piPremeasure_pi_eval

added theorem MeasureTheory.piPremeasure_pi_mono

added theorem MeasureTheory.volume_pi

added theorem MeasureTheory.volume_pi_ball

added theorem MeasureTheory.volume_pi_closedBall

added theorem MeasureTheory.volume_pi_pi

added theorem MeasureTheory.volume_preserving_finTwoArrow

added theorem MeasureTheory.volume_preserving_funUnique

added theorem MeasureTheory.volume_preserving_piEquivPiSubtypeProd

added theorem MeasureTheory.volume_preserving_piFinSuccAboveEquiv

added theorem MeasureTheory.volume_preserving_piFinTwo

added theorem MeasureTheory.volume_preserving_pi_empty

added theorem generateFrom_eq_pi

added theorem generateFrom_pi

added theorem generateFrom_pi_eq

added theorem isPiSystem_pi