Commit 2024-03-13 15:14 46c190e6

feat(Probability/Kernel): add ae_compProd_iff (#11276) Let κ : kernel α β and η : kernel (α × β) γ be two s-finite kernels and p a predicate on β × γ. If the set { x | p x} is measurable, then (∀ᵐ bc ∂(κ ⊗ₖ η) a, p bc) ↔ ∀ᵐ b ∂κ a, ∀ᵐ c ∂η (a, b), p (b, c).