op_inl

Mathlib.CategoryTheory.Limits.Opposites

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

English

In a PullbackCone f g in C, op.inl equals fst.op.

Русский

В PullbackCone f g в C, op.inl равен fst.op.

LaTeX

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

Lean4

theorem op_inl {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.inl = c.fst.op := by simp

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

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

Разделы

Аффилиация

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