eq_of_hom — Mathlib

English

Let X, Y be objects of the discrete category on α and i: X ⟶ Y a morphism. Then the underlying elements agree: X.as = Y.as.

Русский

Пусть X, Y — объекты дискретной категории на α, и i: X ⟶ Y — морфизм. Тогда в основе лежит равенство элементов: X.as = Y.as.

LaTeX

$$$X.{\\text{as}} = Y.{\\text{as}}$$$

Lean4

/-- Extract the equation from a morphism in a discrete category. -/
theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as :=
  i.down.down

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