iIndepSet_of_mem — Mathlib

English

If π_i are pi-systems and for every i, f_i ∈ π_i, with f_i measurable, and π is independent, then iIndepSet f μ holds.

Русский

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

LaTeX

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

Lean4

theorem iIndepSet_of_mem {π : ι → Set (Set Ω)} {f : ι → Set Ω} (hfπ : ∀ i, f i ∈ π i) (hf : ∀ i, MeasurableSet (f i))
    (hπ : iIndepSets π μ) : iIndepSet f μ :=
  Kernel.iIndepSets.iIndepSet_of_mem hfπ hf hπ

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