unop_inr

Mathlib.CategoryTheory.Limits.Opposites

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

English

In a PullbackCone f g in Cᵒᵖ, unop.inr equals snd.unop.

Русский

В PullbackCone f g в Cᵒᵖ, unop.inr равен snd.unop.

LaTeX

$$$$c.{\mathrm{unop}}{\mathrm{inr}} = c.{\mathrm{snd}}.{\mathrm{unop}}.$$$$

Lean4

theorem unop_inr {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.inr = c.snd.unop := by simp

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

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

Разделы

Аффилиация

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