exists_measurable_mem — Mathlib

English

If a filter f is measurably generated and p holds eventually, there exists a measurable set s in f such that p holds on s.

Русский

Если фильтр f измеримо сгенерирован, а свойство p выполняется почти постоянно, то существует измеримое множество s ∈ f такое, что p выполняется на каждом элементе s.

LaTeX

$$$\\\\forall {f : Filter α} [IsMeasurablyGenerated f] {p : α \\rightarrow Prop}, (\\\\kappa) ∃ s \\\\in f, MeasurableSet s \\\\wedge \\\\forall x \\\\in s, p x$$$

Lean4

theorem exists_measurable_mem {f : Filter α} [IsMeasurablyGenerated f] {p : α → Prop} (h : ∀ᶠ x in f, p x) :
    ∃ s ∈ f, MeasurableSet s ∧ ∀ x ∈ s, p x :=
  IsMeasurablyGenerated.exists_measurable_subset h

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