instIsStableUnderRetractsIsoModSerre

Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.instIsStableUnderRetractsIsoModSerre

English

The class P.isoModSerre is stable under retracts: retracts of morphisms with P.isoModSerre also have P.isoModSerre.

Русский

Класс P.isoModSerre устойчив к редукциям: редекты морфизмов с P.isoModSerre тоже удовлетворяют P.isoModSerre.

LaTeX

$$$P.isoModSerre.IsStableUnderRetracts$$$

Lean4

instance : P.isoModSerre.IsStableUnderRetracts :=
  by
  dsimp only [isoModSerre]
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru