English
A Preorder structure is placed on ONote by comparing their formatted representations: x ≤ y iff repr x ≤ repr y, and x < y iff repr x < repr y; reflexivity and transitivity follow from ordinal order.
Русский
На ONote определяется предпорядок через сравнение их форматированных представлений: x ≤ y если repr(x) ≤ repr(y), и x < y если repr(x) < repr(y); рефлексивность и транзитивность следуют из порядка ординалов.
LaTeX
$$$\text{Preorder}(\mathrm{ONote})\;:\; x \le y \iff \mathrm{repr}(x) \le \mathrm{repr}(y),\; x < y \iff \mathrm{repr}(x) < \mathrm{repr}(y).$$$
Lean4
instance : Preorder ONote where
le x y := repr x ≤ repr y
lt x y := repr x < repr y
le_refl _ := @le_refl Ordinal _ _
le_trans _ _ _ := @le_trans Ordinal _ _ _ _
lt_iff_le_not_ge _ _ := @lt_iff_le_not_ge Ordinal _ _ _
