def isSetSemiring_of_isSetAlgebra {α : Type u_1} {𝒜 : Set (Set α)} (h : MeasureTheory.IsSetAlgebra 𝒜) : MeasureTheory.IsSetSemiring 𝒜

Every set algebra is a set semiring: combine the set-ring structure (empty set, closure under union, closure under difference) and view the resulting ring as a semiring.

theorem isSetAlgebra_isPiSystem {α : Type u_1} {𝒜 : Set (Set α)} (h : MeasureTheory.IsSetAlgebra 𝒜) : IsPiSystem 𝒜

A set algebra 𝒜 is automatically a π-system: it is closed under finite intersections.

theorem exists_measure_extension {α : Type u_1} (𝒜 : Set (Set α)) (h𝒜 : MeasureTheory.IsSetAlgebra 𝒜) (μ₀ : MeasureTheory.AddContent ENNReal 𝒜) (hμ₀_sigma : μ₀.IsSigmaSubadditive) : ∃ (μ : MeasureTheory.Measure α), ∀ s ∈ 𝒜, μ s = μ₀ s

Existence part of the Carathéodory extension theorem: any σ-subadditive AddContent μ₀ on a set algebra 𝒜 extends to a measure on the generated σ-algebra σ(𝒜), agreeing with μ₀ on 𝒜.

theorem caratheodory_extension_theorem {α : Type u_1} (𝒜 : Set (Set α)) (h𝒜 : MeasureTheory.IsSetAlgebra 𝒜) (μ₀ : MeasureTheory.AddContent ENNReal 𝒜) (hμ₀_sigma : μ₀.IsSigmaSubadditive) (B : ℕ → Set α) (hB_mem : ∀ (i : ℕ), B i ∈ 𝒜) (hB_cover : ⋃ (i : ℕ), B i = Set.univ) (hB_fin : ∀ (i : ℕ), μ₀ (B i) ≠ ⊤) : ∃! μ : MeasureTheory.Measure α, ∀ s ∈ 𝒜, μ s = μ₀ s

Carathéodory extension theorem. If μ₀ is a σ-finite (witnessed by a cover B : ℕ → 𝒜 with μ₀ (B i) < ∞) σ-subadditive additive content on a set algebra 𝒜, then there exists a unique measure on σ(𝒜) extending μ₀.