comap_id'

Mathlib.Probability.Kernel.Composition.MapComap

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

English

Composing with the identity map yields the same kernel.

Русский

Сочетание с тождественным отображением даёт тот же ядро (kernel).

LaTeX

$$$κ.comap (fun a => a) measurable_id = κ$$$

Lean4

@[simp]
theorem comap_id' (κ : Kernel α β) : comap κ (fun a ↦ a) measurable_id = κ :=
  comap_id κ

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

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

Разделы

Аффилиация

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