isCofilteredOrEmpty_of_directed_ge

English

If α is a preorder with IsDirected α (≥) and Nonempty α, then α is Cofiltered.

Русский

Если α — предранжирование, у которого выполняется направленность относительно ге, и α непусто, то α кофильтрована.

LaTeX

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

Lean4

instance (priority := 100) isCofilteredOrEmpty_of_directed_ge (α : Type u) [Preorder α] [IsDirected α (· ≥ ·)] :
    IsCofilteredOrEmpty α
    where
  cone_objs X
    Y :=
    let ⟨Z, hX, hY⟩ := exists_le_le X Y
    ⟨Z, homOfLE hX, homOfLE hY, trivial⟩
  cone_maps X Y f
    g :=
    ⟨X, 𝟙 _, by
      apply ULift.ext
      subsingleton⟩

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