decidableLE — Mathlib

English

If α has a preorder and a decidable ≤ relation, then WithZero α also has a decidable ≤ relation.

Русский

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

LaTeX

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

Lean4

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

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