English
The integers ℤ are equipped with a linear order, i.e., for any a,b ∈ ℤ, exactly one of a ≤ b or b ≤ a holds, and ≤ is total and antisymmetric.
Русский
Целые числа ℤ образуют линейный порядок: для любых a,b ∈ ℤ верно либо a ≤ b, либо b ≤ a, причём порядок тотальный и антисимметричный.
LaTeX
$$$\forall a,b \in \mathbb{Z}, (a \le b) \lor (b \le a).$$$
Lean4
instance instLinearOrder : LinearOrder ℤ where
le := (· ≤ ·)
le_refl := Int.le_refl
le_trans := @Int.le_trans
le_antisymm := @Int.le_antisymm
lt := (· < ·)
lt_iff_le_not_ge := @Int.lt_iff_le_not_le
le_total := Int.le_total
toDecidableEq := by infer_instance
toDecidableLE := by infer_instance
toDecidableLT := by infer_instance
