join_apply — Mathlib

English

For a measurable set s, the join of m on s equals the integral of μ(s) with respect to m.

Русский

Для измеримого множества s склеивание (join) меры m на s равно интегралу по m от μ(s).

LaTeX

$$$\\text{join } m\\ s = \\int⁻ μ, μ(s) \\, d m$ for measurable $s$.$$

Lean4

@[simp]
theorem join_apply {m : Measure (Measure α)} {s : Set α} (hs : MeasurableSet s) : join m s = ∫⁻ μ, μ s ∂m :=
  Measure.ofMeasurable_apply s hs

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