Commit 2023-02-06 20:02 3afc5839

View on Github →

feat: port MeasureTheory.MeasurableSpaceDef (#2108)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.unionₛ_mem_empty_univ

Created Mathlib/MeasureTheory/MeasurableSpaceDef.lean

added theorem Finset.measurableSet_binterᵢ

added theorem Finset.measurableSet_bunionᵢ

added theorem Measurable.le

added def Measurable

added theorem MeasurableSet.binterᵢ

added theorem MeasurableSet.bunionᵢ_decode₂

added theorem MeasurableSet.compl_iff

added theorem MeasurableSet.congr

added theorem MeasurableSet.empty

added theorem MeasurableSet.interᵢ

added theorem MeasurableSet.interₛ

added theorem MeasurableSet.ite'

added theorem MeasurableSet.singleton

added def MeasurableSet

added inductive MeasurableSpace.GenerateMeasurable

added theorem MeasurableSpace.Top.measurable

added theorem MeasurableSpace.copy_eq

added theorem MeasurableSpace.ext

added theorem MeasurableSpace.ext_iff

added def MeasurableSpace.generateFrom

added theorem MeasurableSpace.generateFrom_induction

added theorem MeasurableSpace.generateFrom_insert_empty

added theorem MeasurableSpace.generateFrom_insert_univ

added theorem MeasurableSpace.generateFrom_le

added theorem MeasurableSpace.generateFrom_le_iff

added theorem MeasurableSpace.generateFrom_measurableSet

added theorem MeasurableSpace.generateFrom_mono

added theorem MeasurableSpace.generateFrom_singleton_empty

added theorem MeasurableSpace.generateFrom_singleton_univ

added theorem MeasurableSpace.generateFrom_sup_generateFrom

added theorem MeasurableSpace.generateFrom_unionᵢ_measurableSet

added def MeasurableSpace.giGenerateFrom

added theorem MeasurableSpace.le_def

added theorem MeasurableSpace.measurableSet_bot_iff

added theorem MeasurableSpace.measurableSet_copy

added theorem MeasurableSpace.measurableSet_generateFrom

added theorem MeasurableSpace.measurableSet_inf

added theorem MeasurableSpace.measurableSet_infᵢ

added theorem MeasurableSpace.measurableSet_infₛ

added theorem MeasurableSpace.measurableSet_injective

added theorem MeasurableSpace.measurableSet_sup

added theorem MeasurableSpace.measurableSet_supᵢ

added theorem MeasurableSpace.measurableSet_supₛ

added theorem MeasurableSpace.measurableSet_top

added theorem MeasurableSpace.measurableSpace_supᵢ_eq

added theorem MeasurableSpace.mkOfClosure_sets

added structure MeasurableSpace

added theorem Set.Countable.measurableSet

added theorem Set.Finite.measurableSet

added theorem Set.Finite.measurableSet_binterᵢ

added theorem Set.Finite.measurableSet_bunionᵢ

added theorem Set.Finite.measurableSet_interₛ

added theorem Set.Finite.measurableSet_unionₛ

added theorem Set.Subsingleton.measurableSet

added theorem Subsingleton.measurableSet

added theorem measurableSet_eq

added theorem measurableSet_insert

added theorem measurable_const

added theorem measurable_id'

added theorem measurable_id

added theorem nonempty_measurable_superset

Modified Mathlib/Topology/Order.lean