eq_traj — Mathlib

English

The map a ↦ trajFun κ a is a measurable family of maps from the product space to the space of trajectories.

Русский

Отображение a ↦ trajFun κ a является измеримым семейством отображений**, из произведения в пространство траекторий.

LaTeX

$$$\\text{Measurable}(\\lambda a.\\ \\mathrm{trajFun}\\;\\kappa\\ a)$$$

Lean4

/-- To check that `η = traj κ a` it is enough to show that the restriction of `η` to variables `≤ b`
is `partialTraj κ a b`. -/
theorem eq_traj {a : ℕ} (η : Kernel (Π i : Iic a, X i) (Π n, X n))
    (hη : ∀ b, η.map (frestrictLe b) = partialTraj κ a b) : η = traj κ a :=
  eq_traj' κ 0 η fun b _ ↦ hη b

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