English
The family of finite-projection marginals given by pi over finite index sets forms a projective limit for the infinite product measure: infinitePiNat μ is the projective limit of the system I ↦ π i μi over finite I.
Русский
Семейство предельных проекций по конечным множителям образует проективный предел для бесконечной цепи: infinitePiNat μ является проективным пределом системы I ↦ π_i μ_i по конечным I.
LaTeX
$$$$IsProjectiveLimit\bigl(\mathrm{infinitePiNat}\,\mu\bigr)\;\bigl(\,I \mapsto \mathrm{Measure.pi}(\lambda i \in I: \mu i)\bigr).$$$$
Lean4
theorem isProjectiveLimit_infinitePiNat :
IsProjectiveLimit (infinitePiNat μ) (fun I : Finset ℕ ↦ (Measure.pi (fun i : I ↦ μ i))) :=
by
intro I
rw [isProjectiveMeasureFamily_pi μ _ _ I.subset_Iic_sup_id, ← restrict₂_comp_restrict I.subset_Iic_sup_id, ← map_map,
← frestrictLe, infinitePiNat, map_comp, traj_map_frestrictLe, partialTraj_const, ← map_comp, ←
compProd_eq_comp_prod, compProd_const, pi_prod_map_IicProdIoc]
all_goals fun_prop
