instPredOrder — Mathlib

English

The integers can be equipped with a PredOrder structure using the standard predecessor function.

Русский

Целым можно наделитьPredOrder-структуру, используя стандартную операцию предшествия.

LaTeX

$$$\text{PredOrder}(\mathbb{Z})$$$

Lean4

@[instance]
abbrev instPredOrder : PredOrder ℤ where
  pred := pred
  pred_le _ := (sub_one_lt_of_le le_rfl).le
  min_of_le_pred ha := ((sub_one_lt_of_le le_rfl).not_ge ha).elim
  le_pred_of_lt {_ _} := le_sub_one_of_lt

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