eventually — Mathlib

English

If f is strongly measurable with respect to a filter, then refining the filter preserves strong measurability along the same measure.

Русский

Если функция сильно измерима относительно фильтра, то уточнение фильтра сохраняет сильную измеримость по той же мере.

LaTeX

$$$ \text{StronglyMeasurableAtFilter}(f,l',\mu) \Leftarrow \text{StronglyMeasurableAtFilter}(f,l,\mu) \text{ when } l' \le l $$$

Lean4

protected theorem eventually (h : StronglyMeasurableAtFilter f l μ) :
    ∀ᶠ s in l.smallSets, AEStronglyMeasurable f (μ.restrict s) :=
  (eventually_smallSets' fun _ _ => AEStronglyMeasurable.mono_set).2 h

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