instIsSFiniteKernelSectLOfProd — Mathlib

English

If κ is IsSFiniteKernel, then κ.sectL b is IsSFiniteKernel for every b (alternate naming path).

Русский

Если κ является IsSFiniteKernel, то κ.sectL b является IsSFiniteKernel для каждого b (альтернативное наименование).

LaTeX

$$$[\\text{IsSFiniteKernel}(κ)] \\Rightarrow \\text{IsSFiniteKernel}(κ.sectL b)$$$

Lean4

instance (κ : Kernel (α × β) γ) (b : β) [IsSFiniteKernel κ] : IsSFiniteKernel (sectL κ b) := by rw [sectL];
  infer_instance

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