Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-25 13:23 cc365b5c

View on Github →

feat(probability/independence): lemmas about pi_Union_Inter of a sequence of singletons (#17013)

Estimated changes

Modified src/measure_theory/pi_system.lean

modified theorem generate_from_pi_Union_Inter_le

modified theorem generate_from_pi_Union_Inter_measurable_set

added theorem generate_from_pi_Union_Inter_singleton_left

modified theorem is_pi_system_pi_Union_Inter

modified theorem le_generate_from_pi_Union_Inter

modified theorem measurable_set_supr_of_mem_pi_Union_Inter

modified theorem mem_pi_Union_Inter_of_measurable_set

modified def pi_Union_Inter

modified theorem pi_Union_Inter_mono_left

added theorem pi_Union_Inter_mono_right

added theorem pi_Union_Inter_singleton

added theorem pi_Union_Inter_singleton_left

modified theorem subset_pi_Union_Inter

Modified src/probability/independence.lean

added theorem probability_theory.Indep_set.indep_generate_from_of_disjoint

added theorem probability_theory.Indep_sets.pi_Union_Inter_of_not_mem

deleted theorem probability_theory.Indep_sets.pi_Union_Inter_singleton

modified theorem probability_theory.indep.symm

modified theorem probability_theory.indep_fun.symm

added theorem probability_theory.indep_sets.bInter

added theorem probability_theory.indep_sets.bUnion

added theorem probability_theory.indep_sets.indep'

modified theorem probability_theory.indep_sets.symm