instRespectsIsoOfIsStableUnderRetracts

Mathlib.CategoryTheory.MorphismProperty.Retract

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.instRespectsIsoOfIsStableUnderRetracts

← MathLib Explorer

English

A RespectsIso instance is established for morphism properties stable under retracts.

Русский

Установлен экземпляр, сохраняющий изоморфизмы для свойств морфизмов, устойчивых к retracts.

LaTeX

$$$P.RespectsIso$$$

Lean4

instance {P : MorphismProperty C} [P.IsStableUnderRetracts] : P.RespectsIso :=
  RespectsIso.of_respects_arrow_iso _ (fun _ _ e ↦ of_retract (Retract.ofIso e.symm))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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