op_singleton

Mathlib.CategoryTheory.ObjectProperty.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.op_singleton

English

The opposite of the singleton X is the singleton of op X.

Русский

Противоположный одиночник X равен одиночнику оп ↦ X.

LaTeX

$$$(\mathrm{singleton} X)^{\mathrm{op}} = \mathrm{singleton}(\mathrm{op} X)$$$

Lean4

@[simp high]
theorem op_singleton (X : C) : (singleton X).op = singleton (op X) := by simp

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

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

Разделы

Аффилиация

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