filter_mono — Mathlib

English

If a function is AEStronglyMeasurable with respect to μ, then it is StronglyMeasurableAtFilter for any filter.

Русский

Если функция AEStronglyMeasurable относительно μ, тогда она сильносильно измерима относительно любого фильтра.

LaTeX

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

Lean4

protected theorem filter_mono (h : StronglyMeasurableAtFilter f l μ) (h' : l' ≤ l) :
    StronglyMeasurableAtFilter f l' μ :=
  let ⟨s, hsl, hs⟩ := h
  ⟨s, h' hsl, hs⟩

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