prod — Mathlib

English

If κ and η are zero-or-Markov kernels, then their product κ ×K η is zero-or-Markov.

Русский

Если ядра κ и η являются нулевыми или Марковскими, то их произведение κ ×K η также нулевое или Марковское.

LaTeX

$$$\\displaystyle (κ \\times_K η) : \\text{IsZeroOrMarkovKernel}$$$

Lean4

nonrec instance prod (κ : Kernel α β) [h : IsZeroOrMarkovKernel κ] (η : Kernel α γ) [IsZeroOrMarkovKernel η] :
    IsZeroOrMarkovKernel (κ ×ₖ η) :=
  by
  rcases eq_zero_or_isMarkovKernel κ with rfl | h
  · simp only [prod]; infer_instance
  rcases eq_zero_or_isMarkovKernel η with rfl | h'
  · simp only [prod]; infer_instance
  infer_instance

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