unop_inl

Mathlib.CategoryTheory.Limits.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.PullbackCone.unop_inl

English

In a PullbackCone f g in Cᵒᵖ, the unop.inl equals fst.unop.

Русский

В PullbackCone f g в Cᵒᵖ, unop.inl равен fst.unop.

LaTeX

$$$$c.{\mathrm{unop}}{\mathrm{inl}} = c.{\mathrm{fst}}.{\mathrm{unop}}.$$$$

Lean4

theorem unop_inl {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.inl = c.fst.unop := by simp

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

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

Разделы

Аффилиация

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