isFilteredOrEmpty_of_semilatticeSup

English

In any nonempty set with a semilattice sup operation, the induced order is filtered.

Русский

В любой непустой множестве с операцией наименьшего верхнего предела (semilattice sup) полученная упорядоченность является фильтрованной.

LaTeX

$$$\forall \alpha, [SemilatticeSup \alpha], [Nonempty \alpha] \,:\; IsFiltered(\alpha)$$$

Lean4

instance (priority := 100) isFilteredOrEmpty_of_semilatticeSup (α : Type u) [SemilatticeSup α] : IsFilteredOrEmpty α
    where
  cocone_objs X Y := ⟨X ⊔ Y, homOfLE le_sup_left, homOfLE le_sup_right, trivial⟩
  cocone_maps X Y f g := ⟨Y, 𝟙 _, by subsingleton⟩

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