const_comp

Mathlib.Probability.Kernel.Composition.CompNotation

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.const_comp

English

For κ : Kernel α (β × γ), (swap β γ) ∘ₖ κ = κ.map Prod.swap.

Русский

Для ядра κ : α → (β × γ) выполняется (swap β γ) ∘ₖ κ = κ.map Prod.swap.

LaTeX

$$$ (\text{swap } β γ) \circ_K κ = κ.map Prod.swap $$$

Lean4

@[simp]
theorem const_comp {ν : Measure β} : (Kernel.const α ν) ∘ₘ μ = μ Set.univ • ν :=
  μ.bind_const

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

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

Разделы

Аффилиация

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