Theorems · Definition · measure theory

piiUnionInter

{α : Type u_3} → {ι : Type u_4} → (ι → Set (Set α)) → Set ι → Set (Set α)

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.

Defined in

Mathlib.MeasureTheory.PiSystem

Cited by

20 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound