pullback_eq_inf — Mathlib

English

The pullback in SemilatticeInf with OrderTop is the infimum: pullback f g = x ⊓ y.

Русский

Прообразный предел в SemilatticeInf с OrderTop равенInf: pullback f g = x ⊓ y.

LaTeX

$$$\text{pullback } f\; g = x \wedge y$$$

Lean4

/-- The pullback in the category of a `SemilatticeInf` with `OrderTop` is the same as the infimum
over the objects.
-/
@[simp]
theorem pullback_eq_inf [SemilatticeInf α] [OrderTop α] {x y z : α} (f : x ⟶ z) (g : y ⟶ z) : pullback f g = x ⊓ y :=
  calc
    pullback f g = limit (cospan f g) := rfl
    _ = Finset.univ.inf (cospan f g).obj := by rw [finite_limit_eq_finset_univ_inf]
    _ = z ⊓ (x ⊓ (y ⊓ ⊤)) := rfl
    _ = z ⊓ (x ⊓ y) := by rw [inf_top_eq]
    _ = x ⊓ y := inf_eq_right.mpr (inf_le_of_left_le f.le)

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