op_inr

Mathlib.CategoryTheory.Limits.Opposites

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

English

In a PullbackCone f g in C, op.inr equals snd.op.

Русский

В PullbackCone f g в C, op.inr равен snd.op.

LaTeX

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

Lean4

theorem op_inr {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.inr = c.snd.op := by simp

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

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

Разделы

Аффилиация

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