proposition: Lemma jBayes_extended (I : finType) (E : I -> {set A}) (F : {set B}) : (forall i j, i != j -> [disjoint E i & E j]) -> cover [set E i | i in I] = [set: A] -> forall i, \Pr_PQ [E i | F] = (\Pr_QP [F | E i] * Pr P (E i)) / \sum_(j in I) \Pr_ QP [F | E j] * Pr P (E j).
proof: Proof. move=> dis cov i; rewrite jBayes; congr (_ / _). move: (@jtotal_prob_cond _ _ QP I F E dis cov). rewrite {1}/QP fdistX1 => ->. by apply eq_bigr => j _; rewrite -/QP {2}/QP fdistX2. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) mathcomp(Rstruct) Reals ssrR realType_ext Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba