Theorem opensMeasurableSpace_iff_forall_measurableSet

Modification history

2023-08-24 13:32
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
feat: the product of Borel spaces is Borel when either of them is second-countable (#6689) …
Added opensMeasurableSpace_iff_forall_measurableSetView on Github →