instBoundedOrder — Mathlib

English

Fin n is a bounded order with bottom 0 and top given by rev 0: bot = 0 and top = rev(0).

Русский

Fin n является ограниченным порядком: наименьшее равно 0, наивысшее равно rev(0).

LaTeX

$$$\mathrm{bot} = 0 \quad\land\quad \mathrm{top} = \mathrm{rev}(0)$$$

Lean4

instance instBoundedOrder [NeZero n] : BoundedOrder (Fin n)
    where
  top := rev 0
  le_top i := Nat.le_pred_of_lt i.is_lt
  bot := 0
  bot_le := Fin.zero_le

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