isSFiniteKernel_sum — Mathlib

English

If ι is countable and every κs(n) is IsSFiniteKernel, then Kernel.sum κs is IsSFiniteKernel.

Русский

Если ι счётно, и каждое κs(n) является IsSFiniteKernel, тогда Kernel.sum κs is IsSFiniteKernel.

LaTeX

$$$IsSFiniteKernel\\left(\\Kernel.sum \\kappa_s\\right).$$$

Lean4

instance isSFiniteKernel_sum [Countable ι] {κs : ι → Kernel α β} [hκs : ∀ n, IsSFiniteKernel (κs n)] :
    IsSFiniteKernel (Kernel.sum κs) := by
  cases fintypeOrInfinite ι
  · rw [sum_fintype]
    exact IsSFiniteKernel.finset_sum Finset.univ fun i _ => hκs i
  cases nonempty_denumerable ι
  exact isSFiniteKernel_sum_of_denumerable hκs

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