instDecidableRel' — Mathlib

English

There is a canonical decidable relation on the product type α×α when α has decidable equality.

Русский

Существует каноническое разрешимое отношение на произведении α×α, когда α имеет разрешимое равенство.

LaTeX

$$$[\\mathrm{DecidableEq}(\\alpha)] \\Rightarrow \\mathrm{DecidableRel}(\\mathrm{HasEquiv.Equiv}(\\alpha \\times \\alpha))$$$

Lean4

instance instDecidableRel' [DecidableEq α] : DecidableRel (HasEquiv.Equiv (α := α × α)) :=
  instDecidableRel

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