English
Let C be a category with a relation r on morphisms. If g1 and g2 are morphisms b → c that are related by CompClosure r, then precomposition with any f: a → b preserves this relation; i.e., f ∘ g1 is CompClosure-related to f ∘ g2.
Русский
Пусть C — категория, задано отношение r на гомоморфизмах. Если g1, g2: b → c связаны через CompClosure r, то при композиции слева с любым f: a → b получаем, что f ∘ g1 и f ∘ g2 также связаны через CompClosure r.
LaTeX
$$$\forall a,b,c\, (f:\, a\to b)\, (g_1,g_2:\, b\to c),\; CompClosure(r,g_1,g_2) \rightarrow CompClosure(r\, , f\circ g_1, f\circ g_2).$$$
Lean4
theorem comp_left {a b c : C} (f : a ⟶ b) : ∀ (g₁ g₂ : b ⟶ c) (_ : CompClosure r g₁ g₂), CompClosure r (f ≫ g₁) (f ≫ g₂)
| _, _, ⟨x, m₁, m₂, y, h⟩ => by simpa using CompClosure.intro (f ≫ x) m₁ m₂ y h
