indepFun_iff_measure_inter_preimage_eq_mul

English

If for each i, f_i ∈ π_i and f_i is measurable, and iIndepSets π μ holds, then iIndepSet f μ.

Русский

Если для каждого i f_i принадлежит π_i и измерим, и iIndepSets(π, μ) держится, то iIndepSet(f, μ).

LaTeX

$$$(\forall i, f_i ∈ π_i) \land (\forall i, MeasurableSet(f_i)) \land iIndepSets(π, μ) \Rightarrow iIndepSet f μ$$$

Lean4

theorem indepFun_iff_measure_inter_preimage_eq_mul {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} :
    IndepFun f g μ ↔ ∀ s t, MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t) := by
  simp only [IndepFun, Kernel.indepFun_iff_measure_inter_preimage_eq_mul, ae_dirac_eq, Filter.eventually_pure,
    Kernel.const_apply]

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