mk₀_surjective

Mathlib.CategoryTheory.ComposableArrows

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.mk₀_surjective

English

Every object in ComposableArrows C 0 arises as mk₀ of some object X; i.e., mk₀ is surjective onto objects.

Русский

У каждого объекта в ComposableArrows C 0 существует предобразователь X: F = mk₀ X.

LaTeX

$$$\forall F : ComposableArrows\ C\ 0, \exists X, F = mk₀ X$$$

Lean4

theorem mk₀_surjective (F : ComposableArrows C 0) : ∃ (X : C), F = mk₀ X :=
  ⟨F.obj' 0, ext₀ rfl⟩

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

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

Разделы

Аффилиация

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