instIsMarkovKernelProdParallelComp

English

If κ and η are Markov kernels, then their parallel composition is also Markov.

Русский

Если κ и η — марковские ядра, то их параллельная композиция также марковска.

LaTeX

$$$$[\\text{IsMarkovKernel } κ] \\; [\\text{IsMarkovKernel } η] \\Rightarrow [\\text{IsMarkovKernel } (κ \\parallelₖ η)].$$$$

Lean4

instance [IsMarkovKernel κ] [IsMarkovKernel η] : IsMarkovKernel (κ ∥ₖ η) :=
  ⟨fun x ↦ ⟨by simp [parallelComp_apply_univ]⟩⟩

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