decidable — Mathlib

English

If r and s are decidable relations (and α has decidable equality), then the lexicographic relation Prod.Lex r s on α × β is decidable.

Русский

Если r и s разрешимы, и у α есть разрешимость равенства, то лексикографическое отношение Prod.Lex r s на α × β разрешимо.

LaTeX

$$$ [DecidableEq \\alpha] \\\\to [DecidableRel r] \\\\to [DecidableRel s] \\\\to DecidableRel (Prod.Lex r s).$$$

Lean4

instance decidable [DecidableEq α] (r : α → α → Prop) (s : β → β → Prop) [DecidableRel r] [DecidableRel s] :
    DecidableRel (Prod.Lex r s) := fun _ _ ↦ decidable_of_decidable_of_iff lex_def.symm

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