English
Same as eq_traj' with possibly different a, n, η and hη; if hη holds, η = traj κ a.
Русский
Та же формула, что и eq_traj', но с иными a, n, η; если выполняется hη, то η = traj κ a.
LaTeX
$$$\\forall {a} {n} (η) (hη : \\forall b \\ge n, η.map (frestrictLe b) = partialTraj κ a b) \\Rightarrow η = traj κ a$$$
Lean4
/-- To check that `η = traj κ a` it is enough to show that the restriction of `η` to variables `≤ b`
is `partialTraj κ a b` for any `b ≥ n`. -/
theorem eq_traj' {a : ℕ} (n : ℕ) (η : Kernel (Π i : Iic a, X i) (Π n, X n))
(hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b) : η = traj κ a :=
by
ext x : 1
refine ((isProjectiveLimit_trajFun _ _ _).unique ?_).symm
rw [isProjectiveLimit_nat_iff' _ _ n]
· intro k hk
rw [inducedFamily_Iic, ← map_apply _ (measurable_frestrictLe k), hη k hk]
· exact isProjectiveMeasureFamily_partialTraj κ x
