comap — Mathlib

English

IsZeroOrMarkovKernel is preserved under comap: if κ is zero or Markov, then comap κ g hg is zero or Markov.

Русский

Свойство нуля или марковского ядра сохраняется под комап: если κ нулевое или марковское, то comap κ g hg также нулевое или марковское.

LaTeX

$$$ \operatorname{IsZeroOrMarkovKernel}( \operatorname{comap}(\kappa, g, hg) ) $$$

Lean4

instance comap (κ : Kernel α β) [IsZeroOrMarkovKernel κ] (hg : Measurable g) : IsZeroOrMarkovKernel (comap κ g hg) :=
  by
  rcases eq_zero_or_isMarkovKernel κ with rfl | h
  · simp only [comap_zero]; infer_instance
  · have := IsMarkovKernel.comap κ hg; infer_instance

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