unop_ofObj

Mathlib.CategoryTheory.ObjectProperty.Opposite

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

English

For any X : ι → Cᵒᵖ, (ofObj X).unop = ofObj (λ i, (X i).unop).

Русский

Для любого X : ι → Cᵒᵖ, (ofObj X).unop = ofObj (λ i, (X i).unop).

LaTeX

$$$\mathrm{ofObj}(X)^{\mathrm{unop}} = \mathrm{ofObj}\big(\lambda i. (X(i))^{\mathrm{unop}}\big)$$$

Lean4

@[simp]
theorem unop_ofObj {ι : Type*} (X : ι → Cᵒᵖ) : (ofObj X).unop = ofObj (fun i ↦ (X i).unop) :=
  op_injective ((op_ofObj _).symm)

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

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

Разделы

Аффилиация

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