meas_inter — Mathlib

English

If f and g are independent, then μ(s ∩ t) = μ(s) μ(t) for measurable s and t with respect to the corresponding pullback sigmas.

Русский

Если f и g независимы, то для измеримых s и t относительно соответствующих сигма-алгебр выполняется μ(s ∩ t) = μ(s) μ(t).

LaTeX

$$$\text{IndepFun}(f,g,μ) \Rightarrow \forall s,t, \text{Measurable}(s) \to \text{Measurable}(t) \Rightarrow μ(s \cap t) = μ(s) μ(t)$$$

Lean4

theorem meas_inter [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) : μ (s ∩ t) = μ s * μ t :=
  (IndepFun_iff _ _ _).1 hfg _ _ hs ht

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