uniq

Mathlib.CategoryTheory.Limits.Shapes.Images

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.HasImage.uniq

English

Uniqueness: if l ≫ F'.m = image.ι f then l = image.lift F'.

Русский

Единственность: если l ≫ F'.m = image.ι f, то l = image.lift F'.

LaTeX

$$$\text{uniq}(F',l,w):\; l = \mathrm{image.lift} F'.$$$

Lean4

theorem uniq (F' : MonoFactorisation f) (l : image f ⟶ F'.I) (w : l ≫ F'.m = image.ι f) : l = image.lift F' :=
  (cancel_mono F'.m).1 (by simp [w])

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

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

Разделы

Аффилиация

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