instIsSFiniteKernelBorelMarkovFromReal

English

If η is s-finite, then borelMarkovFromReal Ω η is s-finite, obtained by comapRight through the embeddingReal Ω.

Русский

Если η является s конечным, то borelMarkovFromReal Ω η также s-конечное, и это достигается через comapRight по embeddingReal Ω.

LaTeX

$$$IsSFiniteKernel(\\mathrm{borelMarkovFromReal}\\,\\Omega\\,\\eta)$$$

Lean4

/-- When `η` is an s-finite kernel, `borelMarkovFromReal Ω η` is an s-finite kernel. -/
instance instIsSFiniteKernelBorelMarkovFromReal (η : Kernel α ℝ) [IsSFiniteKernel η] :
    IsSFiniteKernel (borelMarkovFromReal Ω η) :=
  IsSFiniteKernel.comapRight _ (measurableEmbedding_embeddingReal Ω)

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