Commit 2023-08-24 13:32 82a5026d

View on Github →

feat: the product of Borel spaces is Borel when either of them is second-countable (#6689) We have currently that the product of two Borel spaces is Borel when both of them are second-countable. It is in fact sufficient to assume that only one of them is second-countable. We prove this in this PR. Also move the definition of SecondCountableEither from Function.StronglyMeasurable to BorelSpace.Basic to be able to use it in the statement of the above theorem.

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

modified theorem ContinuousLinearMap.measurable_apply₂

Modified Mathlib/Analysis/Convolution.lean

modified theorem BddAbove.continuous_convolution_left_of_integrable

modified theorem BddAbove.continuous_convolution_right_of_integrable

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

modified theorem Continuous.aemeasurable2

modified theorem Continuous.measurable2

added theorem opensMeasurableSpace_iff_forall_measurableSet

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

modified theorem MeasureTheory.AEEqFun.comp₂Measurable_toGerm

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean