isPiSystem_iUnion_of_directed_le — Mathlib

English

If p is a directed family of π-systems, then the union over n of p(n) is a π-system.

Русский

Если p образует направленную семью π-систем, то их объединение ∪_n p(n) образует π-систему.

LaTeX

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

Lean4

theorem isPiSystem_iUnion_of_directed_le {α ι} (p : ι → Set (Set α)) (hp_pi : ∀ n, IsPiSystem (p n))
    (hp_directed : Directed (· ≤ ·) p) : IsPiSystem (⋃ n, p n) :=
  by
  intro t1 ht1 t2 ht2 h
  rw [Set.mem_iUnion] at ht1 ht2 ⊢
  obtain ⟨n, ht1⟩ := ht1
  obtain ⟨m, ht2⟩ := ht2
  obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m
  exact ⟨k, hp_pi k t1 (hpnk ht1) t2 (hpmk ht2) h⟩

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