decidableLT

Mathlib.Data.Finsupp.Order

URI: https://scilib.ai/kg/mathlib#Finsupp.decidableLT

English

If there is a decidable ≤ on α, then there is a decidable < on ι →₀ α.

Русский

Если существует разрешимый ≤ на α, то существует разрешимый < на ι →₀ α.

LaTeX

$$DecidableLT (ι →₀ α)$$

Lean4

instance decidableLT [DecidableLE α] : DecidableLT (ι →₀ α) :=
  decidableLTOfDecidableLE

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru