instIsZeroOrMarkovKernelProdParallelComp

English

If κ and η are zero-or-Markov, then their parallel composition is zero-or-Markov.

Русский

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

LaTeX

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

Lean4

instance [IsZeroOrMarkovKernel κ] [IsZeroOrMarkovKernel η] : IsZeroOrMarkovKernel (κ ∥ₖ η) :=
  by
  obtain rfl | _ := eq_zero_or_isMarkovKernel κ <;> obtain rfl | _ := eq_zero_or_isMarkovKernel η
  all_goals simpa using by infer_instance

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