of_equivalence

Mathlib.CategoryTheory.Generator.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.HasSeparator.of_equivalence

English

If α: C ≌ D is an equivalence and C has a separator, then D has a separator.

Русский

Если есть эквивалентность между C и D и C имеет разделитель, то D имеет разделитель.

LaTeX

$$$\mathrm{HasSeparator}(D)$$$

Lean4

theorem of_equivalence [HasSeparator C] (α : C ≌ D) : HasSeparator D :=
  ⟨α.functor.obj (separator C), isSeparator_separator C |>.of_equivalence α⟩

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

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

Разделы

Аффилиация

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