isZeroOrProbabilityMeasure — Mathlib

English

Instance: if κ is Markov, then IsZeroOrProbabilityMeasure κ a holds for every a.

Русский

Инстанс: если κ Марковское, тогда IsZeroOrProbabilityMeasure κ a для каждого a.

LaTeX

$$$\forall a, \mathrm{IsZeroOrProbabilityMeasure}(\kappa a)$$$

Lean4

instance (priority := 100) isZeroOrProbabilityMeasure [IsZeroOrMarkovKernel κ] (a : α) :
    IsZeroOrProbabilityMeasure (κ a) :=
  by
  rcases eq_zero_or_isMarkovKernel κ with rfl | h'
  · simp only [Kernel.zero_apply]
    infer_instance
  · infer_instance

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