Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-09-12 23:46 001ffdc4

View on Github →

feat(probability/independence): Independence of singletons (#18506) Characterisation of independence in terms of measure distributing over finite intersections, and lemmas connecting the different concepts of independence. Also add supporting measurable_space and set.preimage lemmas

Estimated changes

Modified src/data/set/basic.lean

added theorem Prop.compl_singleton

Modified src/data/set/image.lean

added theorem set.preimage_singleton_false

added theorem set.preimage_singleton_true

added theorem set.preimage_symm_diff

Modified src/measure_theory/measurable_space.lean

added theorem measurable_embedding.comap_eq

added theorem measurable_embedding.iff_comap_eq

added theorem measurable_equiv.map_eq

added def measurable_equiv.of_involutive

added theorem measurable_equiv.of_involutive_apply

added theorem measurable_equiv.of_involutive_symm

added theorem measurable_mem

added theorem measurable_set_set_of

added theorem measurable_space.comap_compl

added theorem measurable_space.comap_const

added theorem measurable_space.comap_not

added theorem measurable_space.generate_from_singleton

added theorem measurable_space.map_const

added theorem measurable_to_prop

Modified src/measure_theory/measurable_space_def.lean

modified theorem measurable_set.const

modified theorem measurable_space.generate_from_singleton_empty

modified theorem measurable_space.generate_from_singleton_univ

Modified src/probability/independence/basic.lean

added theorem probability_theory.Indep_comap_mem_iff

added theorem probability_theory.Indep_set_iff_Indep_sets_singleton

added theorem probability_theory.Indep_set_iff_measure_Inter_eq_prod

added theorem probability_theory.Indep_sets.Indep_set_of_mem

added theorem probability_theory.Indep_sets.meas_Inter

added theorem probability_theory.Indep_sets_singleton_iff