comap — Mathlib

English

If κ is IsSFiniteKernel, then comap κ g hg is IsSFiniteKernel; in fact, the witness sequence is κ'_n = comap (seq κ n) g hg and sum κ'_n = comap κ g hg.

Русский

Если κ является IsSFiniteKernel, то comap κ g hg тоже IsSFiniteKernel; признак задаётся последовательностью κ'_n = comap (seq κ n) g hg и суммой κ'_n = comap κ g hg.

LaTeX

$$$ \operatorname{IsSFiniteKernel}( \operatorname{comap}(\kappa, g, hg) ) \\text{with } \kappa'_n = \operatorname{comap}(\operatorname{seq} \kappa n) g hg \\text{and } \sum_n \kappa'_n = \operatorname{comap}(\kappa, g, hg) $$$

Lean4

instance comap (κ : Kernel α β) [IsSFiniteKernel κ] (hg : Measurable g) : IsSFiniteKernel (comap κ g hg) :=
  ⟨⟨fun n => Kernel.comap (seq κ n) g hg, inferInstance, (sum_comap_seq κ hg).symm⟩⟩

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