Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-22 22:28 a196f9be

View on Github →

chore(measure_theory/probability_mass_function): Move pmf monad operations into a seperate file (#11579) This PR moves the pure, bind, and bind_on_support operations on pmf into a new probability_mass_function/monad.lean file.

Estimated changes

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.mem_support_bind_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.support_bind
deleted theorem pmf.support_pure
deleted def pmf.bind_on_support
deleted theorem pmf.bind_on_support_apply
deleted theorem pmf.bind_on_support_comm
deleted theorem pmf.bind_on_support_pure
deleted theorem pmf.pure_bind_on_support
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 def pmf.pure
added theorem pmf.pure_apply
added theorem pmf.pure_bind
added theorem pmf.support_bind
added theorem pmf.support_pure