hom_comp — Mathlib

English

The underlying function of the composition f ≫ g is the composition of the underlying functions: f ≫ g corresponds to g ∘ f.

Русский

Базовое отображение композиции f ≫ g равно композиции базовых отображений: g ∘ f.

LaTeX

$$$\forall {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g : X \to Z) = g \circ f$$$

Lean4

theorem hom_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g : ToType X → ToType Z) = g ∘ f :=
  (forget _).map_comp f g

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