decidableLT — Mathlib

English

If α is a preorder and has a decidable less-than relation, then WithZero α has a decidable less-than relation.

Русский

Если у α есть предorder и разрешимо отношение <, то WithZero α также имеет разрешимое отношение <.

LaTeX

$$$\operatorname{Preorder}(\alpha) \land \operatorname{DecidableLT}(\alpha) \Rightarrow \operatorname{DecidableLT}(\mathrm{WithZero}\,\alpha)$$$

Lean4

instance decidableLT [Preorder α] [DecidableLT α] : DecidableLT (WithZero α)
  | _, 0 => isFalse <| by simp
  | 0, (a : α) => isTrue <| by simp
  | (a : α), (b : α) => decidable_of_iff' _ coe_lt_coe

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