IsPiSystem — Mathlib

English

For any set s in α, the image of Iio under s, i.e., Iio '' s, forms a π-system.

Русский

Для любого множества s в α образ множества Iio(s) образует π-систему.

LaTeX

$$$ IsPiSystem\ (Iio''s) $$$

Lean4

/-- A π-system is a collection of subsets of `α` that is closed under binary intersection of
  non-disjoint sets. Usually it is also required that the collection is nonempty, but we don't do
  that here. -/
def IsPiSystem (C : Set (Set α)) : Prop :=
  ∀ᵉ (s ∈ C) (t ∈ C), (s ∩ t : Set α).Nonempty → s ∩ t ∈ C

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