Theorems · Inductive type · measure theory

MeasurableSpace.DynkinSystem

Type u_4 → Type u_4

A Dynkin system is a collection of subsets of a type α that contains the empty set, is closed under complementation and under countable union of pairwise disjoint sets. The disjointness condition is the only difference with σ-algebras. The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras generated by a collection of sets which is stable under intersection. A Dynkin system is also known as a "λ-system" or a "d-system".

Defined in

Mathlib.MeasureTheory.PiSystem

Cited by

19 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms