insert_univ — Mathlib

English

If S is a π-system, then inserting the universal set keeps a π-system.

Русский

Если S — π-система, то добавление множества единицы сохраняет π-систему.

LaTeX

$$$ IsPiSystem\ (insert\ univ\ S) $$$

Lean4

theorem insert_univ {S : Set (Set α)} (h_pi : IsPiSystem S) : IsPiSystem (insert Set.univ S) :=
  by
  intro s hs t ht hst
  rcases hs with hs | hs
  · rcases ht with ht | ht <;> simp [hs, ht]
  · rcases ht with ht | ht
    · simp [hs, ht]
    · exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

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