Theorems · Theorem · measure theory

MeasureTheory.Measure.ext_of_generateFrom_of_cover

∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S T : Set (Set α)},
  m0 = MeasurableSpace.generateFrom S →
    T.Countable →
      IsPiSystem S →
        ⋃₀ T = Set.univ → (∀ t ∈ T, μ t ≠ ⊤) → (∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)) → (∀ t ∈ T, μ t = ν t) → μ = ν

Defined in

Mathlib.MeasureTheory.Measure.Restrict

Cited by

1 results in Mathlib

Foundations

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