instIsIsoPost

Mathlib.CategoryTheory.Limits.Preserves.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsIsoPost

English

There is an instance that the post-limit morphism limit.post F G is an isomorphism.

Русский

Существует экземпляр: limit.post F G является изомормофизмом.

LaTeX

$$$\\text{IsIso}(\\text{limit.post } F G)$$$

Lean4

instance : IsIso (limit.post F G) :=
  show IsIso (preservesLimitIso G F).hom from inferInstance

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

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

Разделы

Аффилиация

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