limit_pre_isIso

Mathlib.CategoryTheory.Limits.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Initial.limit_pre_isIso

← MathLib Explorer

English

For any HasLimit G, the morphism limit.pre G F is an isomorphism.

Русский

Для любого HasLimit G отображение limit.pre G F является изоморфизмом.

LaTeX

$$$\\text{limit.pre}(G,F) \\; \\text{is an isomorphism}.$$$

Lean4

instance limit_pre_isIso [HasLimit G] : IsIso (limit.pre G F) :=
  by
  rw [limit.pre_eq (limitConeComp F (getLimitCone G)) (getLimitCone G)]
  erw [IsLimit.lift_self]
  dsimp
  infer_instance

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

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

Разделы

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

Аффилиация

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