Theorems · Theorem · measure theory

MeasureTheory.Measure.ext_of_generateFrom_of_iUnion

∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (C : Set (Set α)) (B : ℕ → Set α),
  m0 = MeasurableSpace.generateFrom C →
    IsPiSystem C → ⋃ i, B i = Set.univ → (∀ (i : ℕ), B i ∈ C) → (∀ (i : ℕ), μ (B i) ≠ ⊤) → (∀ s ∈ C, μ s = ν s) → μ = ν

Two measures are equal if they are equal on the π-system generating the σ-algebra, and they are both finite on an increasing spanning sequence of sets in the π-system. This lemma is formulated using iUnion. FiniteSpanningSetsIn.ext is a reformulation of this lemma.

Defined in

Mathlib.MeasureTheory.Measure.Restrict

Cited by

1 results in Mathlib

Foundations

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