aemeasurable_uIoc_iff — Mathlib

English

If μ is complete, AEMeasurable f μ is equivalent to Measurable f.

Русский

При полном μ AЕ-измеримость f μ эквивалентна измеримости f.

LaTeX

$$$[\mu \text{ IsComplete}] : \mathrm{AEMeasurable}(f, \mu) \iff \mathrm{Measurable}(f)$$$

Lean4

theorem aemeasurable_uIoc_iff [LinearOrder α] {f : α → β} {a b : α} :
    (AEMeasurable f <| μ.restrict <| Ι a b) ↔
      (AEMeasurable f <| μ.restrict <| Ioc a b) ∧ (AEMeasurable f <| μ.restrict <| Ioc b a) :=
  by rw [uIoc_eq_union, aemeasurable_union_iff]

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