app_zero_eq_comp_π_left — Mathlib

English

In a cofork, two maps into X are equal if they agree after postcomposing with all π_j.

Русский

В кофорке две стрелки в X равны, если согласованы после композиции справа с каждым π_j.

LaTeX

$$$\forall j,\; coend.ι F j ≫ f = coend.ι F j ≫ g \Rightarrow f=g$$$

Lean4

@[simp]
theorem app_zero_eq_comp_π_left (s : Cofork f g) : s.ι.app zero = f ≫ s.π := by
  rw [← s.app_one_eq_π, ← s.w left, parallelPair_map_left]

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