instDecidableEqPresburgerFunc — Mathlib

English

For each natural a, the type FirstOrder.presburgerFunc a carries a decidable equality.

Русский

Для каждого натурального a тип FirstOrder.presburgerFunc a обладает разрешимым равенством.

LaTeX

$$$ \\forall a \\in \\mathbb{N},\\; \\text{DecidableEq} \\big( \\text{FirstOrder.presburgerFunc } a \\big). $$$

Lean4

instance instDecidableEqPresburgerFunc {a✝} : DecidableEq✝ (@FirstOrder.presburgerFunc✝ a✝) :=
  instDecidableEqPresburgerFunc.decEq

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