instLinearOrder — Mathlib

English

The set Fin n carries a linear order inherited from the usual order on natural numbers via the embedding a ↦ a.val.

Русский

Множество Fin n обладает линейным порядком, наследуемым от обычного порядка на натуральных числах через отображение a ↦ a.val.

LaTeX

$$$\mathrm{Fin}(n)\text{ with } a \le b \text{ defined by } a.{val} \le b.{val} \text{ is a linear order}$$$

Lean4

instance instLinearOrder : LinearOrder (Fin n) :=
  Fin.val_injective.linearOrder _ Fin.le_iff_val_le_val Fin.lt_iff_val_lt_val coe_min coe_max compare_eq_compare_val

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