proposition: Lemma mu_cut : forall (A:Type)(m:distr A)(P:set A)(cP f g:MF A), cover P cP -> (forall x, P x -> f x == g x) -> 1<=mu m cP -> mu m f == mu m g.
proof: Proof. intros; apply Oeq_trans with (mu m (fesp cP f)). apply (mu_esp_one m cP f); auto. intros; apply Oeq_trans with (mu m (fesp cP g)). apply mu_stable_eq. simpl; apply ford_eq_intro; intro x; unfold fesp; apply (cover_esp_fun (P:=P) (cP:=cP)); auto. apply Oeq_sym; apply (mu_esp_one m cP g); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)