isSFiniteKernel — Mathlib

English

If κ is finite in the IsFiniteKernel sense, then for every a, κ(a) is SFinite.

Русский

Если κ конечное ядро, то для каждого a ядро κ(a) является SFinite.

LaTeX

$$$[IsFiniteKernel \\\\kappa] \\\\Rightarrow \\\\text{SFinite}(\\\\kappa a) \\\\text{для каждого } a$$$

Lean4

instance (priority := 100) isSFiniteKernel [h : IsFiniteKernel κ] : IsSFiniteKernel κ :=
  ⟨⟨fun n => if n = 0 then κ else 0, fun n => by
      simp only; split_ifs
      · exact h
      · infer_instance, by
      ext a s hs
      rw [Kernel.sum_apply' _ _ hs]
      have : (fun i => ((ite (i = 0) κ 0) a) s) = fun i => ite (i = 0) (κ a s) 0 := by ext1 i; split_ifs <;> rfl
      rw [this, tsum_ite_eq]⟩⟩

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