boundedOrder — Mathlib

English

For a finite type α, the collection of all Finset α, ordered by inclusion, forms a bounded order with top = univ and bottom = ∅.

Русский

Для конечного типа α множество Finset α, упорядоченное по включению, образует ограниченный порядок: верхняя граница — univ, нижняя — ∅.

LaTeX

$$$(\mathrm{Finset} \alpha, \subseteq)$ является ограниченным порядком with top = \mathrm{univ} \text{ and } \bot = \emptyset.$$

Lean4

instance boundedOrder : BoundedOrder (Finset α) :=
  { inferInstanceAs (OrderBot (Finset α)) with
    top := univ
    le_top := subset_univ }

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