English
If each κ_n is a finite kernel, then for all a, b in ℕ the partial trajectory kernel κ a b is finite.
Русский
Если для каждого n ядро κ_n является конечным, то для любых a, b ∈ ℕ ядро частичной траектории κ a b также конечное.
LaTeX
$$$ \forall a,b \in \mathbb{N},\ IsFiniteKernel(\partialTraj\kappa a b) $$$
Lean4
instance [∀ n, IsFiniteKernel (κ n)] (a b : ℕ) : IsFiniteKernel (partialTraj κ a b) :=
by
obtain hab | hba := le_total a b
·
induction b, hab using Nat.le_induction with
| base => rw [partialTraj_self]; infer_instance
| succ k hak => rw [partialTraj_succ_of_le hak]; infer_instance
· rw [partialTraj_le hba]; infer_instance
