Theorems · Theorem · measure theory

MeasureTheory.exists_measurable_superset_forall_eq

∀ {α : Type u_1} {ι : Sort u_5} [inst : MeasurableSpace α] [Countable ι] (μ : ι → MeasureTheory.Measure α) (s : Set α),
  ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i) s

For every set s and a countable collection of measures μ i there exists a measurable superset t ⊇ s such that each measure μ i takes the same value on s and t.

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceCountable