swapRight — Mathlib

English

If κ is a zero-or-Markov kernel, then swapRight κ is also zero-or-Markov.

Русский

Если κ является нулево-или-марковским ядром, то swapRight κ также нулево-или-марковское.

LaTeX

$$$$\\text{IsZeroOrMarkovKernel}(κ) \\Rightarrow \\text{IsZeroOrMarkovKernel}(\\mathrm{swapRight}\\,κ)$$$$

Lean4

instance swapRight (κ : Kernel α (β × γ)) [IsZeroOrMarkovKernel κ] : IsZeroOrMarkovKernel (swapRight κ) := by
  rw [Kernel.swapRight_eq]; infer_instance

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