English
The supremum of two elements in a preorder forms a binary coproduct in the corresponding category.
Русский
Наибольшее (sup) двух элементов в порядке образует бинарный coproduct в соответствующей категории.
LaTeX
$$$ \\text{isColimitBinaryCofan}(X,Y) : IsColimit( BinaryCofan.mk(P:= X \\sup Y, \\mathrm{homOfLE}\\, le\\_sup\\_left, \\mathrm{homOfLE}\\, le\\_sup\\_right)).$$$
Lean4
/-- The supremum of two elements in a preordered type is a binary coproduct
in the category associated to this preorder. -/
def isColimitBinaryCofan (X Y : C) :
IsColimit (BinaryCofan.mk (P := X ⊔ Y) (homOfLE le_sup_left) (homOfLE le_sup_right)) :=
BinaryCofan.isColimitMk (fun s ↦ homOfLE (sup_le (leOfHom s.inl) (leOfHom s.inr))) (by intros; rfl) (by intros; rfl)
(by intros; rfl)
