instBoundedOrder — Mathlib

English

The structure Colex on Finset α carries a bounded order: its top element is toColex(univ) and every element is below this top element in the order.

Русский

У строения Colex на Finset α имеется ограниченный порядок: наивысшая граница равна toColex(univ), и каждый элемент лежит ниже этой вершины в порядке.

LaTeX

$$$\text{BoundedOrder}(\text{Colex}(\text{Finset}\,\alpha)) \;\text{with top }= toColex(\text{univ})$ and $x \le \text{top}$ for all $x$.$$

Lean4

instance instBoundedOrder : BoundedOrder (Colex (Finset α))
    where
  top := toColex univ
  le_top _x := toColex_le_toColex_of_subset <| subset_univ _

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