eventually_filterAt_measurableSet

English

There exists eventual measurability for sets in the Vitali filter at x.

Русский

Существует почти везде измеримость для множеств в фильтре Vitali в точке x.

LaTeX

$$$\\forall x,\\ exists\\ t\\in v.filterAt x,\\ MeasurableSet(t).$$$

Lean4

theorem eventually_filterAt_measurableSet (x : X) : ∀ᶠ t in v.filterAt x, MeasurableSet t := by
  filter_upwards [v.eventually_filterAt_mem_setsAt x] with _ ha using v.measurableSet _ _ ha

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