full_arrow_eq_iff

Mathlib.CategoryTheory.Groupoid.Subgroupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subgroupoid.full_arrow_eq_iff

English

In the full subgroupoid on D, two arrows f and g from c to d are equal if and only if their underlying components are equal.

Русский

В полной подгруппоида на D два стрелы f и g: c ⟶ d равны тогда, когда их составляющие равны.

LaTeX

$$$f = g \\iff f.1 = g.1$$$

Lean4

theorem full_arrow_eq_iff {c d : (full D).objs} {f g : c ⟶ d} : f = g ↔ f.1 = g.1 :=
  Subtype.ext_iff

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

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

Разделы

Аффилиация

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