isProjectiveMeasureFamily_partialTraj

English

For any natural a and any x0, the induced family over b ↦ partialTraj κ a b x0 is a projective measure family.

Русский

Для любого натурального a и любого x0 индуцированное семейство b ↦ partialTraj κ a b x0 образует проективное семейство мер.

LaTeX

$$$\\text{IsProjectiveMeasureFamily}\\bigl(\\text{inducedFamily}(\\lambda b.\\ partialTraj\\ κ\\ a\\ b\\ x_0)\\bigr)$$$

Lean4

theorem isProjectiveMeasureFamily_partialTraj {a : ℕ} (x₀ : Π i : Iic a, X i) :
    IsProjectiveMeasureFamily (inducedFamily (fun b ↦ partialTraj κ a b x₀)) :=
  isProjectiveMeasureFamily_inducedFamily _ (fun _ _ ↦ partialTraj_map_frestrictLe₂_apply (κ := κ) x₀)

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