Commit 2023-09-26 11:46 d84c8d2f

View on Github →

feat: Sigma-algebra generated by a singleton (#2513) Match https://github.com/leanprover-community/mathlib/pull/18506

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

added theorem Prop.compl_singleton

Modified Mathlib/Data/Set/Image.lean

added theorem Set.preimage_singleton_false

added theorem Set.preimage_singleton_true

Modified Mathlib/Init/Function.lean

added theorem Function.comp_def

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem MeasurableEmbedding.comap_eq

added theorem MeasurableEmbedding.iff_comap_eq

added theorem MeasurableEquiv.map_eq

added def MeasurableEquiv.ofInvolutive

added theorem MeasurableEquiv.ofInvolutive_apply

added theorem MeasurableEquiv.ofInvolutive_symm

added theorem MeasurableSpace.comap_compl

added theorem MeasurableSpace.comap_const

added theorem MeasurableSpace.comap_not

added theorem MeasurableSpace.generateFrom_singleton

added theorem MeasurableSpace.map_const

added theorem MeasurableSpace.map_def

added theorem measurableSet_setOf

added theorem measurable_mem

added theorem measurable_to_prop

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean