Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-13 10:27 869cb328

View on Github →

chore(measure_theory/probability_mass_function): Refactor the pmf file into a definitions file and a constructions file (#10298)

Estimated changes

added theorem pmf.apply_eq_zero_iff
added def pmf.bind
added theorem pmf.bind_apply
added theorem pmf.bind_bind
added theorem pmf.bind_comm
added theorem pmf.bind_pure
added theorem pmf.coe_bind_apply
added theorem pmf.coe_le_one
added theorem pmf.has_sum_coe_one
added theorem pmf.mem_support_iff
added def pmf.pure
added theorem pmf.pure_apply
added theorem pmf.pure_bind
added theorem pmf.summable_coe
added def pmf.support
added def pmf.to_measure
added theorem pmf.to_measure_apply'
added theorem pmf.to_measure_apply
added theorem pmf.tsum_coe
added def {u}
deleted def pmf.bind
deleted theorem pmf.bind_apply
deleted theorem pmf.bind_bind
deleted theorem pmf.bind_comm
deleted theorem pmf.bind_pure
deleted theorem pmf.coe_bind_apply
deleted theorem pmf.coe_le_one
deleted theorem pmf.has_sum_coe_one
deleted theorem pmf.mem_support_iff
deleted theorem pmf.mem_support_pure_iff
deleted def pmf.pure
deleted theorem pmf.pure_apply
deleted theorem pmf.pure_bind
deleted theorem pmf.summable_coe
deleted def pmf.support
deleted def pmf.to_measure
deleted theorem pmf.to_measure_apply'
deleted theorem pmf.to_measure_apply
deleted theorem pmf.tsum_coe
deleted def {u}