meas_inter — Mathlib

English

If hf : iIndepFun f κ μ, then iIndep (fun x ↦ (mβ x).comap (f x)) κ μ.

Русский

Если hf : iIndepFun f κ μ, то iIndep (функция x ↦ (mβ x).comap (f x)) κ μ.

LaTeX

$$$ (hf : iIndepFun f κ μ) \\Rightarrow iIndep (\\lambda x. (mβ x).comap (f x)) κ μ $$$

Lean4

theorem meas_inter {β γ : Type*} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] {f : Ω → β} {g : Ω → γ}
    (hfg : IndepFun f g κ μ) {s t : Set Ω} (hs : MeasurableSet[mβ.comap f] s) (ht : MeasurableSet[mγ.comap g] t) :
    ∀ᵐ a ∂μ, κ a (s ∩ t) = κ a s * κ a t :=
  hfg _ _ hs ht

Похожие утверждения