unop_fst — Mathlib

English

For objects X,Y,Z in Cᵒᵖ, with arrows f:X→Y and g:X→Z, and a PushoutCocone c for f,g, the fst component after unop equals the inl component after unop.

Русский

Для объектов X,Y,Z в Cᵒᵖ с стрелами f:X→Y и g:X→Z и кокон-под PushoutCocone c, первый компонент после применения unop совпадает с inl после unop.

LaTeX

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

Lean4

theorem unop_fst {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.fst = c.inl.unop := by simp

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