instIsFiniteKernelSectROfProd

Mathlib.Probability.Kernel.Composition.MapComap

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

English

If κ is a finite kernel, then for every a ∈ α, sectR κ a is finite.

Русский

Если κ — конечное ядро, то для каждого a ∈ α секция sectR κ a тоже конечна.

LaTeX

$$IsFiniteKernel κ ⇒ IsFiniteKernel (sectR κ a)$$

Lean4

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

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

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

Разделы

Аффилиация

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