decidableLE — Mathlib

English

There is a decidable ≤ relation on Localization(s) provided α has a decidable ≤ relation. This gives a computable comparison for any two localized elements.

Русский

На локализации(s) существует разрешимое отношение ≤, если у исходного моноида имеется разрешимое ≤. Это даёт вычислимое сравнение любых двух локализованных элементов.

LaTeX

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

Lean4

@[to_additive]
instance decidableLE [DecidableLE α] : DecidableLE (Localization s) := fun a b =>
  Localization.recOnSubsingleton₂ a b fun _ _ _ _ => decidable_of_iff' _ mk_le_mk

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