Commit 2023-08-15 08:08 17a54df9

View on Github →

feat: intervals with rational bounds generate the real Borel sigma algebra (#6490) Add borel_eq_generateFrom_Ioi_rat, borel_eq_generateFrom_Ici_rat, borel_eq_generateFrom_Iic_rat (we already have the Iio result). Also prove that these sets of intervals are pi-systems.

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean.lean

added theorem le_iff_forall_lt_rat_imp_le

added theorem le_iff_forall_rat_lt_imp_le

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

added theorem Real.borel_eq_generateFrom_Ici_rat

added theorem Real.borel_eq_generateFrom_Iic_rat

added theorem Real.borel_eq_generateFrom_Ioi_rat

added theorem Real.isPiSystem_Ici_rat

added theorem Real.isPiSystem_Iic_rat

added theorem Real.isPiSystem_Iio_rat

added theorem Real.isPiSystem_Ioi_rat

Modified Mathlib/MeasureTheory/PiSystem.lean

added theorem isPiSystem_Ici

added theorem isPiSystem_Iic

added theorem isPiSystem_image_Ici

added theorem isPiSystem_image_Iic

Modified Mathlib/Probability/Kernel/CondCdf.lean

deleted theorem isPiSystem_Ici

deleted theorem isPiSystem_Iic