instDecidableEqRelations — Mathlib

English

There is a DecidableEq instance for the i-th relation type of the sum language, provided a DecidableEq instance on the corresponding component relation type.

Русский

Существует инстанс DecidableEq для отношения i-й компонентной части в суммарном языке, при условии DecidableEq для компоненты.

LaTeX

$$$DecidableEq((\langle f,R \rangle : Language).Relations(i))$$$

Lean4

/-- Passes a `DecidableEq` instance on a type of relation symbols through the  `Language`
constructor. Despite the fact that this is proven by `inferInstance`, it is still needed -
see the `example`s in `ModelTheory/Ring/Basic`. -/
instance instDecidableEqRelations {f : ℕ → Type*} {R : ℕ → Type*} (n : ℕ) [DecidableEq (R n)] :
    DecidableEq ((⟨f, R⟩ : Language).Relations n) :=
  inferInstance

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