snd_comp

Mathlib.Probability.Kernel.Composition.CompMap

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

English

Let κ: Kernel α β and η: Kernel β (γ × δ). Then (η ∘ₖ κ).snd = η.snd ∘ₖ κ.

Русский

Пусть κ: α → β и η: β → (γ × δ). Тогда (η ∘ₖ κ).snd = η.snd ∘ₖ κ.

LaTeX

$$$ (\eta \circ_K \kappa).snd = \eta.snd \circ_K \kappa $$$

Lean4

theorem snd_comp (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η ∘ₖ κ).snd = η.snd ∘ₖ κ := by
  simp_rw [snd_eq, map_comp κ η _]

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

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

Разделы

Аффилиация

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