Theorems · Definition · measure theory

MeasurableSpace.mkOfClosure

{α : Type u_1} → (g : Set (Set α)) → {t | MeasurableSet t} = g → MeasurableSpace α

If g is a collection of subsets of α such that the σ-algebra generated from g contains the same sets as g, then g was already a σ-algebra.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Defs

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses propext, Quot.sound