stronglyMeasurableAtFilter_of_mem

English

If h is StronglyMeasurableAtFilter and l' ≤ l, then h is also StronglyMeasurableAtFilter for l'.

Русский

Если h — сильносильно измерима относительно фильтра, и l' меньше или равно l, то h тоже корректно работает для l'.

LaTeX

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

Lean4

theorem stronglyMeasurableAtFilter_of_mem {s} (h : AEStronglyMeasurable f (μ.restrict s)) (hl : s ∈ l) :
    StronglyMeasurableAtFilter f l μ :=
  ⟨s, hl, h⟩

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