aemeasurable_restrict_of_monotoneOn

English

If a function is monotone on a measurable set s, then its restriction to s is a.e. measurable with respect to μ.restrict s.

Русский

Если функция монотонна на измеримом множестве s, то её ограничение на s является АЕ-измеримой по μ.restrict s.

LaTeX

$$$\text{MeasurableSet}(s) \Rightarrow \text{Measurable} \bigl(f|_{s}\bigr) \text{ for monotoneOn } f \text{ on } s$$$

Lean4

theorem aemeasurable_restrict_of_monotoneOn [LinearOrder β] [OrderClosedTopology β] {μ : Measure β} {s : Set β}
    (hs : MeasurableSet s) {f : β → α} (hf : MonotoneOn f s) : AEMeasurable f (μ.restrict s) :=
  have : Monotone (f ∘ (↑) : s → α) := fun ⟨x, hx⟩ ⟨y, hy⟩ => fun (hxy : x ≤ y) => hf hx hy hxy
  aemeasurable_restrict_of_measurable_subtype hs this.measurable

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