English
The projection to the first coordinate is measurable and the pushforward of μ × ν along fst is μ (quasi-measure-preserving).
Русский
Проекция на первую координату измерима и образ меры μ × ν по fst равен μ (почти сохраняет меру).
LaTeX
$$$\text{QuasiMeasurePreserving}(\text{fst}, (\mu \otimes \nu), \mu)$$$
Lean4
@[fun_prop]
theorem quasiMeasurePreserving_fst : QuasiMeasurePreserving Prod.fst (μ.prod ν) μ :=
by
refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
rw [map_apply measurable_fst hs, ← prod_univ, ← nonpos_iff_eq_zero]
refine (prod_prod_le _ _).trans_eq ?_
rw [h2s, zero_mul]