ofFunOfCountable

Mathlib.Probability.Kernel.Basic

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

Lean4

/-- In a countable space with measurable singletons, every function `α → MeasureTheory.Measure β`
defines a kernel. -/
def ofFunOfCountable [MeasurableSpace α] {_ : MeasurableSpace β} [Countable α] [MeasurableSingletonClass α]
    (f : α → Measure β) : Kernel α β where
  toFun := f
  measurable' := measurable_of_countable f

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

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

Разделы

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

Аффилиация

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