comp_id

Mathlib.Probability.Kernel.Composition.CompMap

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

English

Composing with the identity kernel leaves the kernel unchanged: κ ∘ₖ Kernel.id = κ.

Русский

Сочетание с тождественным ядром не меняет ядро: κ ∘ₖ Kernel.id = κ.

LaTeX

$$$ \kappa \circ_K \text{Kernel.id} = \kappa $$$

Lean4

@[simp]
theorem comp_id (κ : Kernel α β) : κ ∘ₖ Kernel.id = κ := by rw [Kernel.id, comp_deterministic_eq_comap, comap_id]

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

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

Разделы

Аффилиация

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