op_fst

Mathlib.CategoryTheory.Limits.Opposites

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

English

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

Русский

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

LaTeX

$$$$c.op.fst = c.inl.op.$$$$

Lean4

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

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

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

Разделы

Аффилиация

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