map_id

Mathlib.Probability.Kernel.Composition.MapComap

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

English

If κ is finite, η is finite, then (id ∥ η) ∘ (μ ⊗ κ) = μ ⊗ (η ∘ κ).

Русский

Если κ и η конечны, то (id ∥ η) ∘ (μ ⊗ κ) = μ ⊗ (η ∘ κ).

LaTeX

$$$$ (\\text{Kernel.id} \\parallel_k η) \\circ_m (μ ⊗_m κ) = μ ⊗_m (η ∘_k κ). $$$$

Lean4

@[simp]
theorem map_id (κ : Kernel α β) : map κ id = κ := by
  ext a
  simp [map_apply, measurable_id]

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

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

Разделы

Аффилиация

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