Commit 2023-05-21 12:07 11332d53

View on Github →

feat: port MeasureTheory.Constructions.BorelSpace.Basic (#4018)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

added theorem AEMeasurable.coe_ereal_ennreal

added theorem AEMeasurable.coe_nnreal_ennreal

added theorem AEMeasurable.coe_nnreal_real

added theorem AEMeasurable.coe_real_ereal

added theorem AEMeasurable.edist

added theorem AEMeasurable.ennnorm

added theorem AEMeasurable.ennreal_toNNReal

added theorem AEMeasurable.ennreal_toReal

added theorem AEMeasurable.ennreal_tsum

added theorem AEMeasurable.ereal_toReal

added theorem AEMeasurable.isGLB

added theorem AEMeasurable.isLUB

added theorem AEMeasurable.nnnorm

added theorem AEMeasurable.nnreal_tsum

added theorem AEMeasurable.norm

added theorem AEMeasurable.real_toNNReal

added theorem ClosedEmbedding.measurable

added theorem Continuous.aemeasurable2

added theorem Continuous.aemeasurable

added theorem Continuous.borel_measurable

added theorem Continuous.measurable2

added theorem Continuous.measurable

added theorem Continuous.openPosMeasure_map

added theorem ContinuousMap.measurable

added theorem ContinuousOn.measurable_piecewise

added theorem Dense.borel_eq_generateFrom_Ico_mem

added theorem Dense.borel_eq_generateFrom_Ico_mem_aux

added theorem Dense.borel_eq_generateFrom_Ioc_mem

added theorem Dense.borel_eq_generateFrom_Ioc_mem_aux

added def ENNReal.ennrealEquivSum

added theorem ENNReal.measurable_ofReal

added theorem ENNReal.measurable_of_measurable_nnreal

added theorem ENNReal.measurable_of_measurable_nnreal_nnreal

added theorem ENNReal.measurable_of_measurable_nnreal_prod

added theorem ENNReal.measurable_toNNReal

added theorem ENNReal.measurable_toReal

added theorem EReal.measurable_of_measurable_real

added def Homemorph.toMeasurableEquiv

added def Homeomorph.toMeasurableEquiv

added theorem Homeomorph.toMeasurableEquiv_coe

added theorem Homeomorph.toMeasurableEquiv_symm_coe

added theorem IsClosed.measurableSet

added theorem IsCompact.measurableSet

added theorem IsGδ.measurableSet

added theorem IsOpen.measurableSet

added theorem IsPreconnected.measurableSet

added theorem LowerSemicontinuous.measurable

added def Mathlib.Tactic.Borelize.addBorelInstance

added def Mathlib.Tactic.Borelize.borelToRefl

added def Mathlib.Tactic.Borelize.borelize

added theorem Measurable.coe_ereal_ennreal

added theorem Measurable.coe_nnreal_ennreal

added theorem Measurable.coe_nnreal_real

added theorem Measurable.coe_real_ereal

added theorem Measurable.dist

added theorem Measurable.edist

added theorem Measurable.ennnorm

added theorem Measurable.ennreal_ofReal

added theorem Measurable.ennreal_toNNReal

added theorem Measurable.ennreal_toReal

added theorem Measurable.ennreal_tsum'

added theorem Measurable.ennreal_tsum

added theorem Measurable.ereal_toReal

added theorem Measurable.iInf_Prop

added theorem Measurable.iSup_Prop

added theorem Measurable.infDist

added theorem Measurable.infEdist

added theorem Measurable.infNndist

added theorem Measurable.isGLB

added theorem Measurable.isLUB

added theorem Measurable.max

added theorem Measurable.min

added theorem Measurable.nndist

added theorem Measurable.nnnorm

added theorem Measurable.nnreal_tsum

added theorem Measurable.norm

added theorem Measurable.real_toNNReal

added def MeasurableEquiv.ennrealEquivNNReal

added def MeasurableEquiv.erealEquivReal

added theorem MeasurableSet.induction_on_open

added theorem MeasurableSet.nhdsWithin_isMeasurablyGenerated

added theorem MeasureTheory.Measure.ext_of_Ici

added theorem MeasureTheory.Measure.ext_of_Ico'

added theorem MeasureTheory.Measure.ext_of_Ico

added theorem MeasureTheory.Measure.ext_of_Ico_finite

added theorem MeasureTheory.Measure.ext_of_Iic

added theorem MeasureTheory.Measure.ext_of_Ioc'

added theorem MeasureTheory.Measure.ext_of_Ioc

added theorem MeasureTheory.Measure.ext_of_Ioc_finite

added theorem Real.borel_eq_generateFrom_Iio_rat

added theorem Real.borel_eq_generateFrom_Ioo_rat

added def Real.finiteSpanningSetsInIooRat

added theorem Real.isPiSystem_Ioo_rat

added theorem Real.measure_ext_Ioo_rat

added theorem Set.OrdConnected.measurableSet

added theorem TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom

added theorem UpperSemicontinuous.measurable

added theorem aEMeasurable_coe_nnreal_real_iff

added theorem aemeasurable_biInf

added theorem aemeasurable_biSup

added theorem aemeasurable_coe_nnreal_ennreal_iff

added theorem aemeasurable_iInf

added theorem aemeasurable_iSup

added theorem aemeasurable_restrict_of_antitoneOn

added theorem aemeasurable_restrict_of_monotoneOn

added def borel

added theorem borel_comap

added theorem borel_eq_generateFrom_Ici

added theorem borel_eq_generateFrom_Ico

added theorem borel_eq_generateFrom_Iic

added theorem borel_eq_generateFrom_Iio

added theorem borel_eq_generateFrom_Ioc

added theorem borel_eq_generateFrom_Ioi

added theorem borel_eq_generateFrom_isClosed

added theorem borel_eq_generateFrom_of_subbasis

added theorem borel_eq_top_of_countable

added theorem borel_eq_top_of_discrete

added theorem closure_ae_eq_of_null_frontier

added theorem generateFrom_Ico_mem_le_borel

added theorem interior_ae_eq_of_null_frontier

added theorem isPiSystem_isOpen

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_ball

added theorem measurableSet_closedBall

added theorem measurableSet_closure

added theorem measurableSet_eball

added theorem measurableSet_interior

added theorem measurableSet_le'

added theorem measurableSet_le

added theorem measurableSet_lt'

added theorem measurableSet_lt

added theorem measurableSet_of_continuousAt

added theorem measurableSet_of_mem_nhdsWithin_Ioi

added theorem measurableSet_of_mem_nhdsWithin_Ioi_aux

added theorem measurableSet_uIcc

added theorem measurableSet_uIoc

added theorem measurable_biInf

added theorem measurable_biSup

added theorem measurable_cInf

added theorem measurable_cSup

added theorem measurable_ciInf

added theorem measurable_ciSup

added theorem measurable_coe_ennreal_ereal

added theorem measurable_coe_nnreal_ennreal

added theorem measurable_coe_nnreal_ennreal_iff

added theorem measurable_coe_nnreal_real

added theorem measurable_coe_nnreal_real_iff

added theorem measurable_coe_real_ereal

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_ereal_toReal

added theorem measurable_iInf

added theorem measurable_iSup

added theorem measurable_infDist

added theorem measurable_infEdist

added theorem measurable_infNndist

added theorem measurable_liminf'

added theorem measurable_liminf

added theorem measurable_limsup'

added theorem measurable_limsup

added theorem measurable_nndist

added theorem measurable_nnnorm

added theorem measurable_norm

added theorem measurable_of_Ici

added theorem measurable_of_Iic

added theorem measurable_of_Iio

added theorem measurable_of_Ioi

added theorem measurable_of_continuousOn_compl_singleton

added theorem measurable_of_isClosed

added theorem measurable_of_isOpen

added theorem measurable_of_is_closed'

added theorem measurable_real_toNNReal

added theorem measure_closure_of_null_frontier

added theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow

added theorem measure_interior_of_null_frontier

added theorem nullMeasurableSet_lt

added theorem nullMeasurableSet_of_null_frontier

added theorem pi_le_borel_pi

added theorem prod_le_borel_prod

added theorem tendsto_measure_cthickening

added theorem tendsto_measure_cthickening_of_isClosed

added theorem tendsto_measure_cthickening_of_isCompact