Commit 2023-05-11 10:44 eff4459b

View on Github →

feat: port Probability.CondCount (#3889)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/CondCount.lean

added def ProbabilityTheory.condCount

added theorem ProbabilityTheory.condCount_add_compl_eq

added theorem ProbabilityTheory.condCount_compl

added theorem ProbabilityTheory.condCount_disjoint_union

added theorem ProbabilityTheory.condCount_empty

added theorem ProbabilityTheory.condCount_empty_meas

added theorem ProbabilityTheory.condCount_eq_one_of

added theorem ProbabilityTheory.condCount_eq_zero_iff

added theorem ProbabilityTheory.condCount_inter'

added theorem ProbabilityTheory.condCount_inter

added theorem ProbabilityTheory.condCount_inter_self

added theorem ProbabilityTheory.condCount_of_univ

added theorem ProbabilityTheory.condCount_probabilityMeasure

added theorem ProbabilityTheory.condCount_self

added theorem ProbabilityTheory.condCount_singleton

added theorem ProbabilityTheory.condCount_union

added theorem ProbabilityTheory.condCount_univ

added theorem ProbabilityTheory.finite_of_condCount_ne_zero

added theorem ProbabilityTheory.pred_true_of_condCount_eq_one