instHasBinaryCoproductsOfOrderBot

English

The binary coproduct satisfies Limits.coprod x y = x ⊔ y.

Русский

Двухместный копроизвод выполняет равенство coprod x y = x ⊔ y.

LaTeX

$$$\mathrm{Limits.coprod}\; x\; y = x \lor y$$$

Lean4

instance (priority := 100) [SemilatticeSup α] [OrderBot α] : HasBinaryCoproducts α :=
  by
  have : ∀ x y : α, HasColimit (pair x y) :=
    by
    letI := hasFiniteColimits_of_hasFiniteColimits_of_size.{u} α
    infer_instance
  apply hasBinaryCoproducts_of_hasColimit_pair

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