instSFiniteProdCompProd

Mathlib.Probability.Kernel.Composition.MeasureCompProd

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.instSFiniteProdCompProd

English

If μ is a measure on α and κ is a kernel α → β, then μ ⊗ₘ κ is SFinite.

Русский

Если μ — мера на α и κ — ядро α → β, то μ ⊗ₘ κ — есть SFinite.

LaTeX

$$$\\text{SFinite}(\\mu \\otimes_{\\mathrm{m}} \\kappa)$$$

Lean4

instance : SFinite (μ ⊗ₘ κ) := by rw [compProd]; infer_instance

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

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

Разделы

Аффилиация

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