Add lemma `pmf_measurable` #558

Job	Run time
rocq-core	57s
coq	1m 2s
mathcomp-classical	2m 55s
mathcomp-analysis-single	14m 40s
mathcomp-reals	2m 9s
mathcomp-experimental-reals	1m 55s
mathcomp-analysis	12m 46s
mathcomp-reals-stdlib	1m 33s
mathcomp-analysis-stdlib	13m 22s
mathcomp-infotheo	7m 12s
	58m 31s

Provide feedback