Commit 2023-02-11 09:36 9a3cb306

View on Github →

feat: port MeasureTheory.PiSystem (#2160)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/PiSystem.lean

added theorem IsPiSystem.comap

added theorem IsPiSystem.insert_empty

added theorem IsPiSystem.insert_univ

added theorem IsPiSystem.singleton

added def IsPiSystem

added inductive MeasurableSpace.DynkinSystem.GenerateHas

added theorem MeasurableSpace.DynkinSystem.ext

added def MeasurableSpace.DynkinSystem.generate

added theorem MeasurableSpace.DynkinSystem.generateFrom_eq

added theorem MeasurableSpace.DynkinSystem.generateHas_compl

added theorem MeasurableSpace.DynkinSystem.generateHas_def

added theorem MeasurableSpace.DynkinSystem.generate_has_subset_generate_measurable

added theorem MeasurableSpace.DynkinSystem.generate_inter

added theorem MeasurableSpace.DynkinSystem.generate_le

added theorem MeasurableSpace.DynkinSystem.has_compl_iff

added theorem MeasurableSpace.DynkinSystem.has_diff

added theorem MeasurableSpace.DynkinSystem.has_union

added theorem MeasurableSpace.DynkinSystem.has_unionᵢ

added theorem MeasurableSpace.DynkinSystem.has_univ

added theorem MeasurableSpace.DynkinSystem.le_def

added def MeasurableSpace.DynkinSystem.ofMeasurableSpace

added theorem MeasurableSpace.DynkinSystem.ofMeasurableSpace_le_ofMeasurableSpace_iff

added theorem MeasurableSpace.DynkinSystem.ofMeasurableSpace_toMeasurableSpace

added def MeasurableSpace.DynkinSystem.restrictOn

added def MeasurableSpace.DynkinSystem.toMeasurableSpace

added structure MeasurableSpace.DynkinSystem

added theorem MeasurableSpace.induction_on_inter

added theorem MeasurableSpace.isPiSystem_measurableSet

added theorem generateFrom_generatePiSystem_eq

added theorem generateFrom_measurableSet_of_generatePiSystem

added theorem generateFrom_piUnionᵢInter_le

added theorem generateFrom_piUnionᵢInter_measurableSet

added theorem generateFrom_piUnionᵢInter_singleton_left

added inductive generatePiSystem

added theorem generatePiSystem_eq

added theorem generatePiSystem_measurableSet

added theorem generatePiSystem_mono

added theorem generatePiSystem_subset_self

added theorem isPiSystem_Icc

added theorem isPiSystem_Icc_mem

added theorem isPiSystem_Ico

added theorem isPiSystem_Ico_mem

added theorem isPiSystem_Iio

added theorem isPiSystem_Ioc

added theorem isPiSystem_Ioc_mem

added theorem isPiSystem_Ioi

added theorem isPiSystem_Ioo

added theorem isPiSystem_Ioo_mem

added theorem isPiSystem_Ixx

added theorem isPiSystem_Ixx_mem

added theorem isPiSystem_generatePiSystem

added theorem isPiSystem_image_Iio

added theorem isPiSystem_image_Ioi

added theorem isPiSystem_piUnionᵢInter

added theorem isPiSystem_unionᵢ_of_directed_le

added theorem isPiSystem_unionᵢ_of_monotone

added theorem le_generateFrom_piUnionᵢInter

added theorem measurableSet_supᵢ_of_mem_piUnionᵢInter

added theorem mem_generatePiSystem_unionᵢ_elim'

added theorem mem_generatePiSystem_unionᵢ_elim

added theorem mem_piUnionᵢInter_of_measurableSet

added def piUnionᵢInter

added theorem piUnionᵢInter_mono_left

added theorem piUnionᵢInter_mono_right

added theorem piUnionᵢInter_singleton

added theorem piUnionᵢInter_singleton_left

added theorem subset_generatePiSystem_self

added theorem subset_piUnionᵢInter