isCofiltered_of_semilatticeInf_nonempty

English

For every α with SemilatticeInf structure and Nonempty, α is Cofiltered.

Русский

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

LaTeX

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

Lean4

instance (priority := 100) isCofiltered_of_semilatticeInf_nonempty (α : Type u) [SemilatticeInf α] [Nonempty α] :
    IsCofiltered α where

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