parallelComp_zero_left — Mathlib

English

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

Русский

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

LaTeX

$$$$(0 : Kernel α β) ∥ₖ η = 0.$$$$

Lean4

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

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