isFilteredOrEmpty_of_directed_le — Mathlib

English

In a directed preorder, the underlying type is filtered or empty.

Русский

В направленном preorder множество объектов является фильтрованным или пустым.

LaTeX

$$$\forall \alpha [Preorder \alpha] [IsDirected \alpha (\le)] : IsFilteredOrEmpty(\alpha)$$$

Lean4

instance (priority := 100) isFilteredOrEmpty_of_directed_le (α : Type u) [Preorder α] [IsDirected α (· ≤ ·)] :
    IsFilteredOrEmpty α
    where
  cocone_objs X
    Y :=
    let ⟨Z, h1, h2⟩ := exists_ge_ge X Y
    ⟨Z, homOfLE h1, homOfLE h2, trivial⟩
  cocone_maps X Y f g := ⟨Y, 𝟙 _, by subsingleton⟩

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