id — Mathlib · SciLib

English

For any object X, the identity morphism 1_X is a transfinite composition of shape Fin(1) built from arrows in W.

Русский

Для любого объекта X тождественный морифизм 1_X является трансфинитной композицией формы Fin(1) из стрелок, принадлежащих W.

LaTeX

$$$\\forall X,\\; \\text{Id}_X \\text{ is a transfinite composition of shape } Fin(1) \\text{ of arrows in } W$$$

Lean4

/-- The identity of any object is a transfinite composition of shape `Fin 1`. -/
def id (X : C) : W.TransfiniteCompositionOfShape (Fin 1) (𝟙 X) :=
  ofComposableArrows W (.mk₀ X) (by simp)

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