hasFiniteLimits_of_semilatticeInf_orderTop

English

If α is a SemilatticeInf with OrderTop, then HasFiniteLimits α holds, i.e., every finite diagram has a limit in α.

Русский

Если α — полупрямой с операцией Inf и OrderTop, то выполняется HasFiniteLimits α: у каждой конечной диаграммы есть предел.

LaTeX

$$$\text{HasFiniteLimits }\alpha$$$

Lean4

instance (priority := 100) hasFiniteLimits_of_semilatticeInf_orderTop [SemilatticeInf α] [OrderTop α] :
    HasFiniteLimits α :=
  ⟨by
    intro J 𝒥₁ 𝒥₂
    exact { has_limit := fun F => HasLimit.mk (finiteLimitCone F) }⟩
    -- see Note [lower instance priority]

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