aestronglyMeasurable_uIoc_iff — Mathlib

English

AEStronglyMeasurable on μ.restrict(uIoc a b) is equivalent to AEStronglyMeasurable on μ.restrict(Ioc a b) and μ.restrict(Ioc b a).

Русский

AEStronglyMeasurable на ограничении по uIoc эквивалентно AEStronglyMeasurable на ограничениях Ioc.

LaTeX

$$$\text{AEStronglyMeasurable}(f, μ.restrict(uIoc(a,b))) \iff \left( \text{AEStronglyMeasurable}(f, μ.restrict(Ioc(a,b))) \land \text{AEStronglyMeasurable}(f, μ.restrict(Ioc(b,a))) \right).$$$

Lean4

theorem aestronglyMeasurable_uIoc_iff [LinearOrder α] [PseudoMetrizableSpace β] {f : α → β} {a b : α} :
    AEStronglyMeasurable f (μ.restrict <| uIoc a b) ↔
      AEStronglyMeasurable f (μ.restrict <| Ioc a b) ∧ AEStronglyMeasurable f (μ.restrict <| Ioc b a) :=
  by rw [uIoc_eq_union, aestronglyMeasurable_union_iff]

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