Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 12:58 4da939bf

View on Github →

feat(probability_theory/cond_count): use the counting measure to describe probability in the elementary sense (#13484)

Estimated changes

Created src/probability/cond_count.lean

added def probability_theory.cond_count

added theorem probability_theory.cond_count_add_compl_eq

added theorem probability_theory.cond_count_compl

added theorem probability_theory.cond_count_disjoint_union

added theorem probability_theory.cond_count_empty

added theorem probability_theory.cond_count_empty_meas

added theorem probability_theory.cond_count_eq_one_of

added theorem probability_theory.cond_count_eq_zero_iff

added theorem probability_theory.cond_count_inter'

added theorem probability_theory.cond_count_inter

added theorem probability_theory.cond_count_inter_self

added theorem probability_theory.cond_count_is_probability_measure

added theorem probability_theory.cond_count_self

added theorem probability_theory.cond_count_singleton

added theorem probability_theory.cond_count_union

added theorem probability_theory.cond_count_univ

added theorem probability_theory.finite_of_cond_count_ne_zero

added theorem probability_theory.pred_true_of_cond_count_eq_one

Modified src/probability/conditional.lean

added theorem probability_theory.cond_add_cond_compl_eq

modified theorem probability_theory.cond_apply

added theorem probability_theory.cond_cond_eq_cond_inter'

modified theorem probability_theory.cond_cond_eq_cond_inter

added theorem probability_theory.cond_empty

modified theorem probability_theory.cond_eq_inv_mul_cond_mul

added theorem probability_theory.cond_inter_self

added theorem probability_theory.cond_mul_eq_inter'

modified theorem probability_theory.cond_mul_eq_inter

modified theorem probability_theory.cond_pos_of_inter_ne_zero