eq_zero_or_isMarkovKernel — Mathlib

English

Let κ be a kernel with IsZeroOrMarkovKernel structure. Then either κ = 0 or κ is Markov.

Русский

Пусть κ — ядро с структурой IsZeroOrMarkovKernel. Тогда либо κ = 0, либо κ является Марковским ядром.

LaTeX

$$$\kappa = 0 \lor \mathrm{IsMarkovKernel}(\kappa)$$$

Lean4

theorem eq_zero_or_isMarkovKernel (κ : Kernel α β) [h : IsZeroOrMarkovKernel κ] : κ = 0 ∨ IsMarkovKernel κ :=
  h.eq_zero_or_isMarkovKernel'

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