heq_comp — Mathlib

English

If f ≍ f' and g ≍ g', then their compositions are HEq: f ≫ g ≍ f' ≫ g'. This expresses compatibility of HEq with composition.

Русский

Если f ≍ f' и g ≍ g', то их композиции являются HEq: f ≫ g ≍ f' ≫ g'. Это выражает совместимость HEq с композицией.

LaTeX

$$$ (f \\mathrel{\\equiv} f') \\; \\land \\; (g \\mathrel{\\equiv} g') \\; \\Rightarrow \\; (f \\circ g) \\mathrel{\\equiv} (f' \\circ g') $$$

Lean4

theorem heq_comp {C} [Category C] {X Y Z X' Y' Z' : C} {f : X ⟶ Y} {g : Y ⟶ Z} {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'}
    (eq1 : X = X') (eq2 : Y = Y') (eq3 : Z = Z') (H1 : f ≍ f') (H2 : g ≍ g') : f ≫ g ≍ f' ≫ g' := by grind

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