coprod_eq_sup — Mathlib

English

The instance HasBinaryCoproducts α exists under SemilatticeSup α and OrderBot α.

Русский

Существование бинарных копроизводов для α при наличии SemilatticeSup α и OrderBot α.

LaTeX

$$$\text{HasBinaryCoproducts }\alpha$$$

Lean4

/-- The binary coproduct in the category of a `SemilatticeSup` with `OrderBot` is the same as the
supremum.
-/
@[simp]
theorem coprod_eq_sup [SemilatticeSup α] [OrderBot α] (x y : α) : Limits.coprod x y = x ⊔ y :=
  calc
    Limits.coprod x y = colimit (pair x y) := rfl
    _ = Finset.univ.sup (pair x y).obj := by rw [finite_colimit_eq_finset_univ_sup (pair x y)]
    _ = x ⊔ (y ⊔ ⊥) := rfl
    _ = x ⊔ y := by rw [sup_bot_eq]

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