English
If f and g are independent with respect to κ μ, then for measurable sets s, t, the joint measure over s ∩ t equals the product of the marginal measures over s and t, almost surely.
Русский
Если функции f и g независимы относительно κ μ, то для измеримых множеств s, t совместная мера над s ∩ t равна произведению мер по s и t почти наверняка.
LaTeX
$$$ (IndepFun\\ f\\ g\\ κ\\ μ) \\Rightarrow \\forall (s t),\\ MeasurableSet s \\land MeasurableSet t \\Rightarrow \\forall^{{\\mathrm{ae}}} a, κ a (s \\cap t) = κ a s \\cdot κ a t $$$
Lean4
@[symm]
theorem symm {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} {s₁ s₂ : Set (Set Ω)}
(h : IndepSets s₁ s₂ κ μ) : IndepSets s₂ s₁ κ μ :=
by
intro t1 t2 ht1 ht2
filter_upwards [h t2 t1 ht2 ht1] with a ha
rwa [Set.inter_comm, mul_comm]
