instIsFiniteMeasureProdCompProdOfIsFiniteKernel

Mathlib.Probability.Kernel.Composition.MeasureCompProd

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

English

μ ⊗ₘ κ is a finite measure if μ is finite and κ is finite in kernel sense.

Русский

μ ⊗ₘ κ является конечной мерой, если μ конечна и κ конечна как ядро.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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