insert_empty — Mathlib

English

If S is a π-system, then inserting the empty set yields a π-system as well.

Русский

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

LaTeX

$$$ IsPiSystem\ (insert\ ∅\ S) $$$

Lean4

theorem insert_empty {S : Set (Set α)} (h_pi : IsPiSystem S) : IsPiSystem (insert ∅ S) :=
  by
  intro s hs t ht hst
  rcases hs with hs | hs
  · simp [hs]
  · rcases ht with ht | ht
    · simp [ht]
    · exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

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