isFiniteKernel_seq

Mathlib.Probability.Kernel.Defs

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.isFiniteKernel_seq

English

For [IsSFiniteKernel κ], IsFiniteKernel (κ.seq n) holds for each n.

Русский

Для каждого n выполняется IsFiniteKernel (κ.seq n).

LaTeX

$$$[IsSFiniteKernel \\\\kappa] \\\\Rightarrow IsFiniteKernel (\\\\kappa.seq n)$$$

Lean4

instance isFiniteKernel_seq (κ : Kernel α β) [h : IsSFiniteKernel κ] (n : ℕ) : IsFiniteKernel (Kernel.seq κ n) :=
  h.tsum_finite.choose_spec.1 n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru