exists_measurable_mem_of_smallSets

English

If a sequence of smallSets holds eventually, there exists a measurable set in f with the property.

Русский

Если свойство относится к smallSets выполняется почти постоянно, существует измеримое множество внутри f с этим свойством.

LaTeX

$$$\\\\forall {f : Filter α} [IsMeasurablyGenerated f] {p : Set α \\rightarrow Prop}, (\\\\forallᶠ s \\\\in f.smallSets, p s) \\\\Rightarrow \\\\exists s \\\\in f, MeasurableSet s \\\\wedge p s$$$

Lean4

theorem exists_measurable_mem_of_smallSets {f : Filter α} [IsMeasurablyGenerated f] {p : Set α → Prop}
    (h : ∀ᶠ s in f.smallSets, p s) : ∃ s ∈ f, MeasurableSet s ∧ p s :=
  let ⟨_s, hsf, hs⟩ := eventually_smallSets.1 h
  let ⟨t, htf, htm, hts⟩ := IsMeasurablyGenerated.exists_measurable_subset hsf
  ⟨t, htf, htm, hs t hts⟩

Похожие утверждения