id_comp

Mathlib.Probability.Kernel.Composition.CompMap

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

English

Composing any kernel with the identity kernel leaves the kernel unchanged.

Русский

Составление ядра с тождественным ядром не изменяет ядро.

LaTeX

$$$\text{Kernel.id} \circ κ = κ$$$

Lean4

@[simp]
theorem id_comp (κ : Kernel α β) : Kernel.id ∘ₖ κ = κ := by rw [Kernel.id, deterministic_comp_eq_map, map_id]

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

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

Разделы

Аффилиация

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