instIsMarkovKernelSectROfProd

Mathlib.Probability.Kernel.Composition.MapComap

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

English

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

Русский

Если κ является ядром Маркова, то для каждого a ∈ α ядро sectR κ a тоже является ядром Маркова.

LaTeX

$$IsMarkovKernel κ ⇒ IsMarkovKernel (sectR κ a)$$

Lean4

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

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

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

Разделы

Аффилиация

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