instRespectsOfIsStableUnderComposition

English

There is a canonical instance giving that W.Respects W whenever W is stable under composition.

Русский

Существует каноничный экземпляр: W уважает сам себя, если он стабилен по композиции.

LaTeX

$$W.Respects W$$

Lean4

instance (priority := 900) (W : MorphismProperty C) [W.IsStableUnderComposition] : W.Respects W
    where
  precomp _ hi _ hf := W.comp_mem _ _ hi hf
  postcomp _ hi _ hf := W.comp_mem _ _ hf hi

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