aemeasurable_restrict_of_antitoneOn

English

Let μ be a measure on β, s a measurable subset, and f: β → α be antitone on s. Then f is almost everywhere measurable with respect to μ restricted to s.

Русский

Пусть μ — мера на β, s — измеримое подмножество, и f: β → α антитоническая на s. Тогда f почти всюду измерима относительно ограничения μ на s.

LaTeX

$$MeasurableSet s → AntitoneOn f s → AEMeasurable f (μ.restrict s)$$

Lean4

theorem aemeasurable_restrict_of_antitoneOn [LinearOrder β] [OrderClosedTopology β] {μ : Measure β} {s : Set β}
    (hs : MeasurableSet s) {f : β → α} (hf : AntitoneOn f s) : AEMeasurable f (μ.restrict s) :=
  @aemeasurable_restrict_of_monotoneOn αᵒᵈ β _ _ ‹_› _ _ _ _ _ ‹_› _ _ _ _ hs _ hf

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