id_mem — Mathlib

English

Every ContainsIdentities morphism property contains identity morphisms: for every object X, id_X belongs to W.

Русский

Любое свойство MorphismProperty, содержащее идентичности, содержит тождественные морфизмы: для каждого X выполнено id_X ∈ W.

LaTeX

$$$\\forall X,\\ W(\\mathrm{id}_X)$$$

Lean4

theorem id_mem (W : MorphismProperty C) [W.ContainsIdentities] (X : C) : W (𝟙 X) :=
  ContainsIdentities.id_mem X

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