snd_map_swap — Mathlib

English

Swapping coordinates and projecting to the second coordinate yields the first marginal of the original measure.

Русский

При перестановке координат и проекции на вторую координату получаем исходную первую маргинальную меру.

LaTeX

$$(ρ.map Prod.swap).snd = ρ.fst$$

Lean4

@[simp]
theorem snd_map_swap : (ρ.map Prod.swap).snd = ρ.fst :=
  by
  rw [Measure.snd, Measure.map_map measurable_snd measurable_swap]
  rfl

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