unop_snd

Mathlib.CategoryTheory.Limits.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.PushoutCocone.unop_snd

English

Similarly, the snd component after unop equals the inr component after unop in PushoutCocone f g.

Русский

Аналогично, второй компонент после применения unop равен inr после unop в PushoutCocone f g.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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