instDecidableEqOfDecidableRelIsConj

English

If IsConj is decidable, then ConjClasses α has decidable equality.

Русский

Если relation IsConj разрешима (решима), то для ConjClasses α имеется разрешимое равенство.

LaTeX

$$$[DecidableRel(IsConj)] \Rightarrow \text{DecidableEq}(\mathrm{ConjClasses}(\alpha))$$$

Lean4

instance [DecidableRel (IsConj : α → α → Prop)] : DecidableEq (ConjClasses α) :=
  inferInstanceAs <| DecidableEq <| Quotient (IsConj.setoid α)

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