isPiSystem_iUnion_of_monotone — Mathlib

English

If p is a monotone family of sets with each p(n) a π-system, then the union over n is a π-system.

Русский

Если p — монотонная семейство множеств, каждое p(n) является π–системой, то их объединение ∪_n является π–системой.

LaTeX

$$$ IsPiSystem\ (⋃ n, p n) $$$

Lean4

theorem isPiSystem_iUnion_of_monotone {α ι} [SemilatticeSup ι] (p : ι → Set (Set α)) (hp_pi : ∀ n, IsPiSystem (p n))
    (hp_mono : Monotone p) : IsPiSystem (⋃ n, p n) :=
  isPiSystem_iUnion_of_directed_le p hp_pi (Monotone.directed_le hp_mono)

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