comp_right — Mathlib

English

If g: b → c and f1, f2: a → b are CompClosure-related, then postcomposition with g preserves this relation: f1 ≫ g and f2 ≫ g are CompClosure-related.

Русский

Если g: b → c и f1, f2: a → b связаны через CompClosure, то постпоследовательная композиция с g сохраняет эту связь: f1 ≫ g и f2 ≫ g связаны через CompClosure.

LaTeX

$$$\forall a,b,c\, (g:\, b\to c)\, (f_1,f_2:\, a\to b),\; CompClosure(r,f_1,f_2) \rightarrow CompClosure(r, f_1\circ g, f_2\circ g).$$$

Lean4

theorem comp_right {a b c : C} (g : b ⟶ c) :
    ∀ (f₁ f₂ : a ⟶ b) (_ : CompClosure r f₁ f₂), CompClosure r (f₁ ≫ g) (f₂ ≫ g)
  | _, _, ⟨x, m₁, m₂, y, h⟩ => by simpa using CompClosure.intro x m₁ m₂ (y ≫ g) h

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