Commit 2023-03-10 09:55 4ac69b29

View on Github →

feat(probability/probability_mass_function): basic lawful monad lemmas for pmf. (#18469) This file adds basic lemmas for monadic operations on pmf, mirroring the lemmas for is_lawful_monad.

Estimated changes

Modified src/probability/probability_mass_function/basic.lean

added theorem pmf.coe_ne_zero

added theorem pmf.ext_iff

added theorem pmf.support_nonempty

Modified src/probability/probability_mass_function/constructions.lean

added theorem pmf.bind_map

added theorem pmf.map_bind

modified theorem pmf.map_comp

added theorem pmf.map_const

modified theorem pmf.map_id

modified theorem pmf.pure_map

Modified src/probability/probability_mass_function/monad.lean

added theorem pmf.bind_const

added theorem pmf.pure_apply_of_ne

added theorem pmf.pure_apply_self