ι_π_ne — Mathlib

English

If j ≠ j', then the composition from the j-th injection to the j'-th projection is zero.

Русский

Если j не равно j', композиция инъекции в j и проекции на j' равна нулю.

LaTeX

$$$\forall J\, f\; [HasBiproduct f] \; \{j,j'\}: J,\; j \neq j' \Rightarrow biproduct.ι\, f\, j \; \gg\; biproduct.π\, f\, j' = 0$$$

Lean4

@[reassoc]
theorem ι_π_ne (f : J → C) [HasBiproduct f] {j j' : J} (h : j ≠ j') : biproduct.ι f j ≫ biproduct.π f j' = 0 := by
  simp [h]

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