Commit 2024-05-18 13:04 964b1427

View on Github →

chore(MeasureTheory.Constructions.BorelSpace.Basic): split file (#12470) The file MeasureTheory.Constructions.BorelSpace.Basic was approximately 2500 lines long. There is somewhat independent content related to order topologies, metrics, and reals, ennreals, and nnreals. This PR proposes to spilt the file according to those boundaries: Basic < Order < Real < Metric. (Short module docstring summaries are added to the new files.)

Estimated changes

deleted theorem AEMeasurable.edist
deleted theorem AEMeasurable.ennnorm
deleted theorem AEMeasurable.ennreal_tsum
deleted theorem AEMeasurable.ereal_toReal
deleted theorem AEMeasurable.isGLB
deleted theorem AEMeasurable.isLUB
deleted theorem AEMeasurable.nnnorm
deleted theorem AEMeasurable.nnreal_tsum
deleted theorem AEMeasurable.norm
deleted theorem ENNReal.measurable_ofReal
deleted theorem ENNReal.measurable_toReal
deleted theorem Measurable.coe_real_ereal
deleted theorem Measurable.dist
deleted theorem Measurable.edist
deleted theorem Measurable.ennnorm
deleted theorem Measurable.ennreal_ofReal
deleted theorem Measurable.ennreal_toReal
deleted theorem Measurable.ennreal_tsum'
deleted theorem Measurable.ennreal_tsum
deleted theorem Measurable.ereal_toReal
deleted theorem Measurable.iInf_Prop
deleted theorem Measurable.iSup_Prop
deleted theorem Measurable.infDist
deleted theorem Measurable.infEdist
deleted theorem Measurable.infNndist
deleted theorem Measurable.isGLB
deleted theorem Measurable.isGLB_of_mem
deleted theorem Measurable.isLUB
deleted theorem Measurable.isLUB_of_mem
deleted theorem Measurable.max
deleted theorem Measurable.min
deleted theorem Measurable.nndist
deleted theorem Measurable.nnnorm
deleted theorem Measurable.nnreal_tsum
deleted theorem Measurable.norm
deleted theorem Measurable.real_toNNReal
deleted theorem Real.isPiSystem_Ici_rat
deleted theorem Real.isPiSystem_Iic_rat
deleted theorem Real.isPiSystem_Iio_rat
deleted theorem Real.isPiSystem_Ioi_rat
deleted theorem Real.isPiSystem_Ioo_rat
deleted theorem Real.measure_ext_Ioo_rat
deleted theorem aemeasurable_biInf
deleted theorem aemeasurable_biSup
deleted theorem aemeasurable_iInf
deleted theorem aemeasurable_iSup
deleted theorem borel_eq_generateFrom_Ici
deleted theorem borel_eq_generateFrom_Ico
deleted theorem borel_eq_generateFrom_Iic
deleted theorem borel_eq_generateFrom_Iio
deleted theorem borel_eq_generateFrom_Ioc
deleted theorem borel_eq_generateFrom_Ioi
deleted theorem measurableSet_Icc
deleted theorem measurableSet_Ici
deleted theorem measurableSet_Ico
deleted theorem measurableSet_Iic
deleted theorem measurableSet_Iio
deleted theorem measurableSet_Ioc
deleted theorem measurableSet_Ioi
deleted theorem measurableSet_Ioo
deleted theorem measurableSet_ball
deleted theorem measurableSet_closedBall
deleted theorem measurableSet_eball
deleted theorem measurableSet_le'
deleted theorem measurableSet_le
deleted theorem measurableSet_lt'
deleted theorem measurableSet_lt
deleted theorem measurableSet_uIcc
deleted theorem measurableSet_uIoc
deleted theorem measurable_biInf
deleted theorem measurable_biSup
deleted theorem measurable_coe_real_ereal
deleted theorem measurable_dist
deleted theorem measurable_edist
deleted theorem measurable_edist_left
deleted theorem measurable_edist_right
deleted theorem measurable_ennnorm
deleted theorem measurable_ereal_toReal
deleted theorem measurable_iInf
deleted theorem measurable_iSup
deleted theorem measurable_infDist
deleted theorem measurable_infEdist
deleted theorem measurable_infNndist
deleted theorem measurable_liminf'
deleted theorem measurable_liminf
deleted theorem measurable_limsup'
deleted theorem measurable_limsup
deleted theorem measurable_nndist
deleted theorem measurable_nnnorm
deleted theorem measurable_norm
deleted theorem measurable_of_Ici
deleted theorem measurable_of_Iic
deleted theorem measurable_of_Iio
deleted theorem measurable_of_Ioi
deleted theorem measurable_real_toNNReal
deleted theorem measurable_sInf
deleted theorem measurable_sSup
deleted theorem nullMeasurableSet_le
deleted theorem nullMeasurableSet_lt'
deleted theorem nullMeasurableSet_lt
added theorem AEMeasurable.edist
added theorem AEMeasurable.ennnorm
added theorem AEMeasurable.nnnorm
added theorem AEMeasurable.norm
added theorem Measurable.dist
added theorem Measurable.edist
added theorem Measurable.ennnorm
added theorem Measurable.infDist
added theorem Measurable.infEdist
added theorem Measurable.infNndist
added theorem Measurable.nndist
added theorem Measurable.nnnorm
added theorem Measurable.norm
added theorem measurableSet_ball
added theorem measurableSet_eball
added theorem measurable_dist
added theorem measurable_edist
added theorem measurable_edist_left
added theorem measurable_edist_right
added theorem measurable_ennnorm
added theorem measurable_infDist
added theorem measurable_infEdist
added theorem measurable_infNndist
added theorem measurable_nndist
added theorem measurable_nnnorm
added theorem measurable_norm
added theorem AEMeasurable.isGLB
added theorem AEMeasurable.isLUB
added theorem Measurable.iInf_Prop
added theorem Measurable.iSup_Prop
added theorem Measurable.isGLB
added theorem Measurable.isLUB
added theorem Measurable.max
added theorem Measurable.min
added theorem aemeasurable_biInf
added theorem aemeasurable_biSup
added theorem aemeasurable_iInf
added theorem aemeasurable_iSup
added theorem measurableSet_Icc
added theorem measurableSet_Ici
added theorem measurableSet_Ico
added theorem measurableSet_Iic
added theorem measurableSet_Iio
added theorem measurableSet_Ioc
added theorem measurableSet_Ioi
added theorem measurableSet_Ioo
added theorem measurableSet_le'
added theorem measurableSet_le
added theorem measurableSet_lt'
added theorem measurableSet_lt
added theorem measurableSet_uIcc
added theorem measurableSet_uIoc
added theorem measurable_biInf
added theorem measurable_biSup
added theorem measurable_iInf
added theorem measurable_iSup
added theorem measurable_liminf'
added theorem measurable_liminf
added theorem measurable_limsup'
added theorem measurable_limsup
added theorem measurable_of_Ici
added theorem measurable_of_Iic
added theorem measurable_of_Iio
added theorem measurable_of_Ioi
added theorem measurable_sInf
added theorem measurable_sSup
added theorem nullMeasurableSet_le
added theorem nullMeasurableSet_lt'
added theorem nullMeasurableSet_lt
added theorem Measurable.nnreal_tsum