Theorems · Theorem · measure theory

Filter.Eventually.exists_measurable_mem_of_smallSets

∀ {α : Type u_1} [inst : MeasurableSpace α] {f : Filter α} [f.IsMeasurablyGenerated] {p : Set α → Prop},
  (∀ᶠ (s : Set α) in f.smallSets, p s) → ∃ s ∈ f, MeasurableSet s ∧ p s

Defined in

Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceFilter.IsMeasurablyGenerated