measurable

Mathlib.Probability.Kernel.Defs

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

English

Let κ be a kernel from α to β. Then the map a ↦ κ a is measurable (as a function from α to the space of measures on β).

Русский

Пусть κ — ядро из α в β. Тогда отображение a ↦ κ a измеримо как функция из α в множество мер β.

LaTeX

$$$\mathrm{Measurable}(\kappa)$$$

Lean4

@[fun_prop]
theorem measurable (κ : Kernel α β) : Measurable κ :=
  κ.measurable'

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

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

Разделы

Аффилиация

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