traj_apply — Mathlib

English

traj κ a x equals trajFun κ a x for all a and x; i.e., the trajectory kernel agrees with the trajectory function on arguments.

Русский

traj κ a x равно trajFun κ a x; ядро траектории согласуется с функцией траектории на аргументах.

LaTeX

$$$\\forall a, x:\\ ProbabilityTheory.Kernel.traj\\ κ\\ a\\ x =\\ ProbabilityTheory.Kernel.trajFun\\ κ\\ a\\ x$$$

Lean4

theorem traj_apply (a : ℕ) (x : Π i : Iic a, X i) : traj κ a x = trajFun κ a x :=
  rfl

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