indepFun_iff_measure_inter_preimage_eq_mul

English

If the sets f_i are measurable, the iIndepSet property is equivalent to iIndepSets for the singleton families {f_i}.

Русский

Если множества f_i измеримы, то свойство iIndepSet эквивалентно свойству iIndepSets для единичных множеств {f_i}.

LaTeX

$$$iIndepSet f κ μ \Leftrightarrow iIndepSets (\lambda i, {f_i}) κ μ$$$

Lean4

theorem indepFun_iff_measure_inter_preimage_eq_mul {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} :
    IndepFun f g κ μ ↔
      ∀ s t, MeasurableSet s → MeasurableSet t → ∀ᵐ a ∂μ, κ a (f ⁻¹' s ∩ g ⁻¹' t) = κ a (f ⁻¹' s) * κ a (g ⁻¹' t) :=
  by
  constructor <;> intro h
  · refine fun s t hs ht => h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩
  · rintro _ _ ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩; exact h s t hs ht

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