compProd_add_left — Mathlib

English

For a family of kernels κ_i: α → β indexed by a countable set ι, and η: α × β → γ, the composite sum κ_i ⊗ η equals the sum over i of (κ_i ⊗ η).

Русский

Для семейства ядер κ_i: α → β индексации счетного множества ι и η: α × β → γ имеем (∑_i κ_i) ⊗ η = ∑_i (κ_i ⊗ η).

LaTeX

$$$$ \\mathrm{Kernel.sum}\\ i \\; (κ_i) \\otimes_{\\kern-0.2em} η \;=\; (\\mathrm{Kernel.sum}\\ i \\; κ_i) \\otimes_{\\kern-0.2em} η. $$$$

Lean4

theorem compProd_add_left (μ κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel μ] [IsSFiniteKernel κ] :
    (μ + κ) ⊗ₖ η = μ ⊗ₖ η + κ ⊗ₖ η := by
  by_cases hη : IsSFiniteKernel η
  · ext _ _ hs
    simp [compProd_apply hs]
  · simp [hη]

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