fst_comp

Mathlib.Probability.Kernel.Composition.CompMap

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

English

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

Русский

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

LaTeX

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

Lean4

theorem fst_comp (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η ∘ₖ κ).fst = η.fst ∘ₖ κ := by simp [fst_eq, map_comp κ η _]

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

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

Разделы

Аффилиация

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