Existence_and_Uniqueness_of_Sigma_Algebra_Generated_by_Collection_of_Subsets

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikisigma-algebras

Let $X$ be a set. Let $\mathcal G \subseteq \powerset X$ be a collection of subsets of $X$ . Then $\map \sigma {\mathcal G}$ , the $\sigma$ -algebra generated by $\mathcal G$ , exists and is unique.

Preamble

import Mathlib.MeasureTheory.MeasurableSpace.Basic

Formal statement

theorem Existence_and_Uniqueness_of_Sigma_Algebra_Generated_by_Collection_of_Subsets {α : Type _} (C : Set (Set α)) : ∃! σ : MeasurableSpace α, (∀ s ∈ C, MeasurableSet s) ∧ ∀ σ' : MeasurableSpace α, (∀ s ∈ C, @MeasurableSet α σ' s) → σ ≤ σ' := by sorry

Source

https://proofwiki.org/wiki/Existence_and_Uniqueness_of_Sigma-Algebra_Generated_by_Collection_of_Subsets

View graph