instDecidableEqOrderRel

Mathlib.ModelTheory.Order

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.instDecidableEqOrderRel

English

For every a, the relation orderRel a has a decidable equality.

Русский

Для каждой пары a выполняется, что отношение orderRel a имеет разрешимое равенство.

LaTeX

$${a : Nat} → DecidableEq (FirstOrder.Language.orderRel a) $$

Lean4

instance instDecidableEqOrderRel {a✝} : DecidableEq✝ (@FirstOrder.Language.orderRel✝ a✝) :=
  instDecidableEqOrderRel.decEq

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

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

Разделы

Аффилиация

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