toDecidableEq — Mathlib

English

There is a canonical DecidableEq instance for F when α is finite and β has DecidableEq, making F decidable equality by comparing underlying functions.

Русский

Существует каноническое решение DecidableEq для F, если α конечно, β имеет DecidableEq; сравнение функций задано по основе.

LaTeX

$$$[DecidableEq\ β] [Fintype\ α] [Fintype\ α] [FunLike\ F\ α\ β] \Rightarrow DecidableEq\ F$$$

Lean4

instance (priority := 100) toDecidableEq {F α β : Type*} [DecidableEq β] [Fintype α] [FunLike F α β] : DecidableEq F :=
  fun a b ↦ decidable_of_iff ((a : α → β) = b) DFunLike.coe_injective.eq_iff

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