pushout_eq_sup — Mathlib

English

The pushout in SemilatticeSup with OrderBot is the supremum: pushout f g = x ⊔ y.

Русский

Копностный схлопиватель в SemilatticeSup с OrderBot равен супремуму: pushout f g = x ⊔ y.

LaTeX

$$$\text{pushout } f\; g = x \lor y$$$

Lean4

/-- The pushout in the category of a `SemilatticeSup` with `OrderBot` is the same as the supremum
over the objects.
-/
@[simp]
theorem pushout_eq_sup [SemilatticeSup α] [OrderBot α] (x y z : α) (f : z ⟶ x) (g : z ⟶ y) : pushout f g = x ⊔ y :=
  calc
    pushout f g = colimit (span f g) := rfl
    _ = Finset.univ.sup (span f g).obj := by rw [finite_colimit_eq_finset_univ_sup]
    _ = z ⊔ (x ⊔ (y ⊔ ⊥)) := rfl
    _ = z ⊔ (x ⊔ y) := by rw [sup_bot_eq]
    _ = x ⊔ y := sup_eq_right.mpr (le_sup_of_le_left f.le)

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