isCofilteredOrEmpty_of_semilatticeInf

English

For every α, if α is a SemilatticeInf and Nonempty, then α is Cofiltered.

Русский

Для любого α, если α имеет полуструктуру инфимы (SemilatticeInf) и непусто, то α кофильтрована.

LaTeX

$$$\\forall \\alpha\\ [\\text{SemilatticeInf } \\alpha] \\ [\\text{Nonempty } \\alpha], \\operatorname{IsCofiltered}(\\alpha).$$$

Lean4

instance (priority := 100) isCofilteredOrEmpty_of_semilatticeInf (α : Type u) [SemilatticeInf α] : IsCofilteredOrEmpty α
    where
  cone_objs X Y := ⟨X ⊓ Y, homOfLE inf_le_left, homOfLE inf_le_right, trivial⟩
  cone_maps X Y f
    g :=
    ⟨X, 𝟙 _, by
      apply ULift.ext
      subsingleton⟩

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