instIsFiniteKernelBorelMarkovFromReal

English

If η is a finite kernel, then borelMarkovFromReal Ω η is finite.

Русский

Если η конечное ядро, то borelMarkovFromReal Ω η является конечным.

LaTeX

$$$IsFiniteKernel(\\mathrm{borelMarkovFromReal}\\,Ω\\,η)$$$

Lean4

/-- When `η` is a finite kernel, `borelMarkovFromReal Ω η` is a finite kernel. -/
instance instIsFiniteKernelBorelMarkovFromReal (η : Kernel α ℝ) [IsFiniteKernel η] :
    IsFiniteKernel (borelMarkovFromReal Ω η) :=
  IsFiniteKernel.comapRight _ (measurableEmbedding_embeddingReal Ω)

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