comp_toUnit — Mathlib

English

For every morphism f: X → Y, composing f with the unit map on Y equals the unit map on X.

Русский

Для каждого морфизма f: X → Y композиция f с единичной картой на Y равна единичной карте на X.

LaTeX

$$$f \\circ \\operatorname{toUnit}(Y) = \\operatorname{toUnit}(X)$$$

Lean4

@[reassoc (attr := simp)]
theorem comp_toUnit {X Y : C} (f : X ⟶ Y) : f ≫ toUnit Y = toUnit X :=
  toUnit_unique _ _

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