decidableLT — Mathlib

English

There is a decidable < relation on Localization(s) when α has a decidable < relation, allowing strict order comparisons to be decided algorithmically.

Русский

Существует разрешимое отношение < на локализации(s), если у α есть такое же отношение <, что позволяет алгоритмически сравнивать элементы по строгому порядку.

LaTeX

$$$\\text{DecidableLT}(\\operatorname{Localization}(s))$$$

Lean4

@[to_additive]
instance decidableLT [DecidableLT α] : DecidableLT (Localization s) := fun a b =>
  Localization.recOnSubsingleton₂ a b fun _ _ _ _ => decidable_of_iff' _ mk_lt_mk

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