Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-31 14:19 39014ec9

View on Github →

feat(probability/independence): add indep_bot_left and indep_bot_right (#16309) Prove that for any m, indep m ⊥ μ, and prove the corresponding statement with bot on the left. Also declare two types as variables on top of the file and remove them from many lemmas.

Estimated changes

Modified src/probability/independence.lean

modified theorem probability_theory.Indep.Indep_sets

modified theorem probability_theory.Indep.indep

modified def probability_theory.Indep

modified theorem probability_theory.Indep_fun.indep_fun

modified def probability_theory.Indep_fun

modified def probability_theory.Indep_set

modified theorem probability_theory.Indep_sets.indep_sets

modified def probability_theory.Indep_sets

modified theorem probability_theory.indep.indep_sets

modified theorem probability_theory.indep.symm

modified def probability_theory.indep

added theorem probability_theory.indep_bot_left

added theorem probability_theory.indep_bot_right

modified def probability_theory.indep_fun

modified theorem probability_theory.indep_of_indep_of_le_left

modified theorem probability_theory.indep_of_indep_of_le_right

modified def probability_theory.indep_set

modified theorem probability_theory.indep_sets.Inter

modified theorem probability_theory.indep_sets.Union

modified theorem probability_theory.indep_sets.indep

modified theorem probability_theory.indep_sets.inter

modified theorem probability_theory.indep_sets.symm

modified theorem probability_theory.indep_sets.union

modified theorem probability_theory.indep_sets.union_iff

modified def probability_theory.indep_sets

modified theorem probability_theory.indep_sets_of_indep_sets_of_le_left

modified theorem probability_theory.indep_sets_of_indep_sets_of_le_right

modified theorem probability_theory.indep_sets_singleton_iff