snd_map_prodMk — Mathlib

English

If X is measurable, then the second marginal of μ.map(a ↦ (X(a), Y(a))) equals μ.map(Y).

Русский

Если X измерима, то вторая маргинальная мера образа μ по a ↦ (X(a), Y(a)) равна μ.map(Y).

LaTeX

$$ (Measurable X) ⇒ snd(μ.map(a ↦ (X(a), Y(a)))) = μ.map Y$$

Lean4

theorem snd_map_prodMk {X : α → β} {Y : α → γ} {μ : Measure α} (hX : Measurable X) :
    (μ.map fun a => (X a, Y a)).snd = μ.map Y :=
  snd_map_prodMk₀ hX.aemeasurable

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