imageMap

Mathlib.CategoryTheory.Limits.Shapes.Images

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.HasImageMap.imageMap

Lean4

/-- Obtain an `ImageMap` from a `HasImageMap` instance. -/
def imageMap {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g) [HasImageMap sq] : ImageMap sq :=
  Classical.choice <|
    @HasImageMap.has_image_map _ _ _ _ _ _ sq
      _
        -- see Note [lower instance priority]

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

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

Разделы

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

Аффилиация

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