measurable_measure — Mathlib

English

Let μ: α → M(β) be a family of measures on β. Then μ is measurable if and only if for every measurable set s ⊆ β, the map a ↦ μ(a)(s) is measurable.

Русский

Пусть μ: α → M(β) задаёт семейство мер на β. Тогда μ измеримо тогда и только если для каждого измеримого множества s ⊆ β функция a ↦ μ(a)(s) измерима.

LaTeX

$$$\\text{Measurable }\\mu \\iff \\forall s,\\ MeasurableSet(s) \\rightarrow \\ Measurable\\ (\\lambda b. \\mu(b)(s)).$$$

Lean4

theorem measurable_measure {μ : α → Measure β} :
    Measurable μ ↔ ∀ (s : Set β), MeasurableSet s → Measurable fun b => μ b s :=
  ⟨fun hμ _s hs => (measurable_coe hs).comp hμ, measurable_of_measurable_coe μ⟩

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