prod_eq_inf — Mathlib

English

The binary product satisfies Limits.prod x y = x ⊓ y.

Русский

Двухместный произведение удовлетворяет равенству вхождения: prod x y = x ⊓ y.

LaTeX

$$$\mathrm{Limits.prod}\; x\; y = x \wedge y$$$

Lean4

/-- The binary product in the category of a `SemilatticeInf` with `OrderTop` is the same as the
infimum.
-/
@[simp]
theorem prod_eq_inf [SemilatticeInf α] [OrderTop α] (x y : α) : Limits.prod x y = x ⊓ y :=
  calc
    Limits.prod x y = limit (pair x y) := rfl
    _ = Finset.univ.inf (pair x y).obj := by rw [finite_limit_eq_finset_univ_inf (pair.{u} x y)]
    _ = x ⊓ (y ⊓ ⊤) := rfl
    _ = x ⊓ y := by
      rw [inf_top_eq]
        -- see Note [lower instance priority]

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