piiUnionInter_of_notMem — Mathlib

English

Let π be a family of pi-systems of subsets of Ω and μ a measure. For a finite set S of indices and an index a not in S, the collection piiUnionInter(π, S) is independent from the collection π(a) with respect to μ.

Русский

Пусть π — семья π-систем подмножеств пространства Ω, и μ — мера. Для конечного множества индексов S и индекса a, не принадлежащего S, совокупность piiUnionInter(π, S) независима от π(a) по отношению к μ.

LaTeX

$$$(iIndepSets\ π\ μ) \land (a \notin S) \Rightarrow IndepSets\bigl(\mathrm{piiUnionInter}(π,S), π(a)\bigr)\ μ$$$

Lean4

theorem piiUnionInter_of_notMem {π : ι → Set (Set Ω)} {a : ι} {S : Finset ι} (hp_ind : iIndepSets π μ) (haS : a ∉ S) :
    IndepSets (piiUnionInter π S) (π a) μ :=
  Kernel.iIndepSets.piiUnionInter_of_notMem hp_ind haS

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