comp — Mathlib

English

If η and κ are s-finite kernels, then their composition η ∘ₖ κ is s-finite.

Русский

Если η и κ — s- конечные ядра, то их композиция η ∘ₖ κ — s- конечна.

LaTeX

$$$\text{IsSFiniteKernel}(\eta) \land \text{IsSFiniteKernel}(\kappa) \Rightarrow \text{IsSFiniteKernel}(\eta \circ_K \kappa)$$$

Lean4

instance comp (η : Kernel β γ) [IsSFiniteKernel η] (κ : Kernel α β) [IsSFiniteKernel κ] : IsSFiniteKernel (η ∘ₖ κ) :=
  by
  simp_rw [← kernel_sum_seq κ, ← kernel_sum_seq η, comp_sum_left, comp_sum_right]
  infer_instance

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