Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-04 21:18 09273ae0

View on Github →

feat(measure_theory/probability_mass_function): Generalize bind on pmfs to binding on the support (#6210)

Estimated changes

Modified src/measure_theory/probability_mass_function.lean

added def pmf.bind_on_support

added theorem pmf.bind_on_support_apply

added theorem pmf.bind_on_support_bind_on_support

added theorem pmf.bind_on_support_comm

added theorem pmf.bind_on_support_eq_bind

added theorem pmf.bind_on_support_eq_zero_iff

added theorem pmf.bind_on_support_pure

added theorem pmf.coe_bind_on_support_apply

added theorem pmf.mem_support_bind_on_support_iff

added theorem pmf.mem_support_pure_iff

added theorem pmf.pure_bind_on_support

Modified src/topology/algebra/infinite_sum.lean

modified theorem tsum_congr

added theorem tsum_dite_left

added theorem tsum_dite_right

added theorem tsum_ne_zero_iff