Theorems · Theorem · measure theory

MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup

∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s →
    ∀ {t : Set α}, MeasurableSet t → (μ.restrict (⋃ i, s i)) t = ⨆ i, (μ.restrict (s i)) t

Defined in

Mathlib.MeasureTheory.Measure.Restrict

Cited by

3 results in Mathlib

Foundations

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

Assumes

Countable