English
μ ⊗ₘ κ is a zero-or-probability measure if μ is zero-or-probability and κ is zero-or-Markov.
Русский
μ ⊗ₘ κ является нуль-или-вероятностной мерой, если μ нуль-или-вероятностна и κ нуль-или-марковое ядро.
LaTeX
$$$[\\text{IsZeroOrProbabilityMeasure}(\\mu)] \\rightarrow [\\text{IsZeroOrMarkovKernel}(\\kappa)] \\Rightarrow \\text{IsZeroOrProbabilityMeasure}(\\mu \\otimes_{\\mathrm{m}} \\kappa)$$$
Lean4
instance [IsZeroOrProbabilityMeasure μ] [IsZeroOrMarkovKernel κ] : IsZeroOrProbabilityMeasure (μ ⊗ₘ κ) :=
by
rw [compProd]
exact IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure ()
