def

Mathlib.CategoryTheory.Generator.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsSeparator.def

English

The symbol «def» in the Separator namespace is an alias for the main definition

Русский

Символ «def» в пространстве IsSeparator — это псевдоним к основному определению

LaTeX

$$$$\text{«def»} = (\text{isSeparator_def} _).1.$$$$

Lean4

theorem «def» {G : C} : IsSeparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = h ≫ g) → f = g :=
  (isSeparator_def _).1

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

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

Разделы

Аффилиация

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