aemeasurable_of_aemeasurable_trim

English

If f is AEMeasurable with μ.trim hm and hm ≤ m0, then f is AEMeasurable with μ.

Русский

Если f — AЕ-измеримая относительно μ.trim hm и hm ≤ m0, то f — AЕ-измеримая относительно μ.

LaTeX

$$$\mathrm{AEMeasurable}(f, \mu\text{.trim}(hm)) \rightarrow \mathrm{AEMeasurable}(f, \mu)$$$

Lean4

theorem aemeasurable_of_aemeasurable_trim {α} {m m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0) {f : α → β}
    (hf : AEMeasurable f (μ.trim hm)) : AEMeasurable f μ :=
  ⟨hf.mk f, Measurable.mono hf.measurable_mk hm le_rfl, ae_eq_of_ae_eq_trim hf.ae_eq_mk⟩

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