English
Under a reindexing equivalence e, map (piCongrLeft X e) of infinitePi μ equals infinitePi μ.
Русский
При переиндексации e отображение (piCongrLeft X e) от infinitePi μ даёт infinitePi μ.
LaTeX
$$$$\mathrm{map}(\mathrm{piCongrLeft}\;X\;e) (\mathrm{infinitePi}\;μ) = \mathrm{infinitePi}\;μ.$$$$
Lean4
/-- If we push the product measure forward by a reindexing equivalence, we get a product measure
on the reindexed product. -/
theorem infinitePi_map_piCongrLeft {α : Type*} (e : α ≃ ι) :
(infinitePi (fun i ↦ μ (e i))).map (piCongrLeft X e) = infinitePi μ :=
by
refine eq_infinitePi μ fun s t ht ↦ ?_
conv_lhs => enter [2, 1]; rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]
rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi, prod_equiv e]
· simp
· simp
· simp_all
· fun_prop
· exact .pi ((countable_toSet _).image e) (by simp_all)
