add — Mathlib

English

If κ and η are IsSFiniteKernel kernels, then κ + η is IsSFiniteKernel.

Русский

Если κ и η являются ядрами IsSFiniteKernel, то κ + η тоже является IsSFiniteKernel.

LaTeX

$$$[IsSFiniteKernel \\\\kappa] \\\\Rightarrow [IsSFiniteKernel \\\\eta] \\\\Rightarrow IsSFiniteKernel (\\\\kappa + \\\\eta)$$$

Lean4

instance add (κ η : Kernel α β) [IsSFiniteKernel κ] [IsSFiniteKernel η] : IsSFiniteKernel (κ + η) :=
  by
  refine ⟨⟨fun n => seq κ n + seq η n, fun n => inferInstance, ?_⟩⟩
  rw [sum_add, kernel_sum_seq κ, kernel_sum_seq η]

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