English
Let π be a family of families of sets: π: ι → Set(Set α). For a subset S of ι, define piiUnionInter π S to be the collection of all sets that can be written as ⋂ x ∈ t f(x) for some finite t ⊆ S and choices f(x) ∈ π(x). In particular, if π is a family of π-systems, then piiUnionInter π S is again a π-system.
Русский
Пусть π : ι → множество(множества α) — семейство π‑систем. Для подмножества S ⊆ ι определим piiUnionInter π S как множество всех множеств, которые можно записать как ⋂ x ∈ t f(x) для некоторого конечного множества t ⊆ S и выбора f(x) ∈ π(x). В частности, если каждое π(x) является π‑системой, то piiUnionInter π S также является π‑системой.
LaTeX
$$$\ piiUnionInter(\pi, S) = \{ s \subseteq α \mid ∃ t : Finset\ ι, (↑t ⊆ S) ∧ ∃ f : ι → Set α, ∀ x, x ∈ t → f(x) ∈ π(x), s = \bigcap_{x ∈ t} f(x) \}$$$
Lean4
/-- From a set of indices `S : Set ι` and a family of sets of sets `π : ι → Set (Set α)`,
define the set of sets that can be written as `⋂ x ∈ t, f x` for some finset `t ⊆ S` and sets
`f x ∈ π x`. If `π` is a family of π-systems, then it is a π-system. -/
def piiUnionInter (π : ι → Set (Set α)) (S : Set ι) : Set (Set α) :=
{s : Set α | ∃ (t : Finset ι) (_ : ↑t ⊆ S) (f : ι → Set α) (_ : ∀ x, x ∈ t → f x ∈ π x), s = ⋂ x ∈ t, f x}
