measurable_coe

Mathlib.Probability.Kernel.Defs

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

← MathLib Explorer

English

If y' belongs to the measurable atom of y, then κ(y') = κ(y).

Русский

Если y' принадлежит измеримому атому y, то κ(y') = κ(y).

LaTeX

$$$y' \\in measurableAtom(y) \\Rightarrow κ(y') = κ(y)$$$

Lean4

protected theorem measurable_coe (κ : Kernel α β) {s : Set β} (hs : MeasurableSet s) : Measurable fun a => κ a s :=
  (Measure.measurable_coe hs).comp κ.measurable

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

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

Разделы

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

Аффилиация

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