instIsSFiniteKernelSectROfProd

Mathlib.Probability.Kernel.Composition.MapComap

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

English

If κ is an S-finite kernel, then sectR κ a is S-finite for any a ∈ α.

Русский

Если κ—S-конечное ядро, то sectR κ a тоже S-конечное для любого a.

LaTeX

$$IsSFiniteKernel κ ⇒ IsSFiniteKernel (sectR κ a)$$

Lean4

instance (κ : Kernel (α × β) γ) (a : α) [IsSFiniteKernel κ] : IsSFiniteKernel (sectR κ a) := by rw [sectR];
  infer_instance

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

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

Разделы

Аффилиация

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