condition — Mathlib

English

To check coequalizing property, it suffices to check it for the second leg.

Русский

Чтобы проверить свойство ко-равенства, достаточно проверить по второй ножке.

LaTeX

$$∀W,k,l,h, Cofork.π s ≫ k = Cofork.π s ≫ l ⇒ ∀ j, s.ι.app j ≫ k = s.ι.app j ≫ l$$

Lean4

@[reassoc (attr := simp)]
theorem condition (t : Cofork f g) : f ≫ t.π = g ≫ t.π := by
  rw [← t.app_zero_eq_comp_π_left, ← t.app_zero_eq_comp_π_right]

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