snd_map_prod_id

Mathlib.Probability.Kernel.Composition.MapComap

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

← MathLib Explorer

English

If f is a measurable function β → γ, then snd (map κ (f x, x)) = κ for any kernel κ : α → β.

Русский

Если f: β→γ измерима, то snd map κ (f x, x) = κ.

LaTeX

$$$snd (map κ (\\lambda a. \\{ fst := f a, snd := a \\})) = κ$$$

Lean4

theorem snd_map_prod_id (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : snd (map κ (fun a ↦ (f a, a))) = κ := by
  rw [snd_map_prod _ hf, Kernel.map_id']

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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