unop_singleton

Mathlib.CategoryTheory.ObjectProperty.Opposite

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

English

For X in Cᵒᵖ, (singleton X).unop = singleton(X.unop).

Русский

Для X ∈ Cᵒᵖ, (singleton X).unop = singleton(X.unop).

LaTeX

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

Lean4

@[simp high]
theorem unop_singleton (X : Cᵒᵖ) : (singleton X).unop = singleton X.unop := by simp

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

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

Разделы

Аффилиация

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