parallelComp_zero_right — Mathlib

English

If the right kernel is the zero kernel, then their parallel composition is the zero kernel.

Русский

Если правое ядро равно нулю, то их параллельная композиция равна нулю.

LaTeX

$$$$κ ∥ₖ (0 : Kernel γ δ) = 0.$$$$

Lean4

@[simp]
theorem parallelComp_zero_right (κ : Kernel α β) : κ ∥ₖ (0 : Kernel γ δ) = 0 :=
  by
  by_cases h : IsSFiniteKernel κ
  · ext; simp [parallelComp_apply]
  · exact parallelComp_of_not_isSFiniteKernel_left _ h

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