fst_swapRight

Mathlib.Probability.Kernel.Composition.MapComap

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

← MathLib Explorer

English

fst(swapRight κ) = snd κ for κ : Kernel α (β × γ).

Русский

fst(swapRight κ) = snd κ для κ: ядро α → β × γ.

LaTeX

$$$\\mathrm{fst}(\\mathrm{swapRight}(κ)) = \\mathrm{snd}(κ)$$$

Lean4

@[simp]
theorem fst_swapRight (κ : Kernel α (β × γ)) : fst (swapRight κ) = snd κ :=
  by
  ext a s hs
  rw [fst_apply' _ _ hs, swapRight_apply', snd_apply' _ _ hs]
  · rfl
  · exact measurable_fst hs

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

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

Разделы

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

Аффилиация

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