measurable_coe — Mathlib

English

For any measurable s ⊆ α × β, (μ.prod ν)(s) = toNNReal (∫⁻ x, ν.toMeasure (Prod.mk x⁻¹' s) ∂μ).

Русский

Для любой измеримой части s ⊆ α × β, (μ.prod ν)(s) равно toNNReal от интеграла ∫⁻ x ν.toMeasure (Prod.mk x⁻¹' s) по μ.

LaTeX

$$$ (\mu \mathrm{prod} \nu)(s) = \operatorname{toNNReal}\left(\int^{-} x\, \nu.toMeasure (\mathrm{Prod.mk} x^{-1} s) \partial \mu\right)$$$

Lean4

theorem measurable_coe {s : Set α} (hs : MeasurableSet s) : Measurable fun μ : Measure α => μ s :=
  Measurable.of_comap_le <| le_iSup_of_le s <| le_iSup_of_le hs <| le_rfl

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