instDecidableLE_1 — Mathlib

English

If α has decidable linear order, then NonemptyInterval α also has a decidable linear order; the proof uses a definable lifting of ≤ from α.

Русский

Если на α дано разрешимое отношение порядка, тогда и NonemptyInterval α обладает разрешимым порядком; доказательство строится через восприятие ≤ из α.

LaTeX

$$$[\text{DecidableLE }\alpha] \Rightarrow \text{DecidableLE}(\mathrm{NonemptyInterval}(\alpha))$$$

Lean4

instance [DecidableLE α] : DecidableLE (NonemptyInterval α) := fun _ _ => decidable_of_iff' _ le_def

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