snd_eq

Mathlib.Probability.Kernel.Composition.MapComap

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

English

For any kernel κ : α → β × γ, snd κ is equal to the pushforward of κ along the second projection: snd κ = map κ Prod.snd.

Русский

Для любого ядра κ : α → β × γ, snd κ равно образу ядра κ по второй проекции: snd κ = map κ Prod.snd.

LaTeX

$$$snd κ = map κ \\mathrm{Prod.snd}$$$

Lean4

theorem snd_eq (κ : Kernel α (β × γ)) : snd κ = map κ Prod.snd := by simp [snd]

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

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

Разделы

Аффилиация

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