instDecidableRel — Mathlib

English

Given DecidableEq α and Finite α, the relation Rel on α induces a decidable relation on Sym2 α.

Русский

При наличии DecidableEq для α и α конечного, отношение Rel на α порождает разрешимое отношение на Sym2 α.

LaTeX

$$$\\forall \\alpha\\; [\\mathrm{DecidableEq}(\\alpha)]\\;\\Rightarrow \\mathrm{DecidableRel}(\\mathrm{Rel}\\;\\alpha)$$$

Lean4

/-- Given `[DecidableEq α]` and `[Fintype α]`, the following instance gives `Fintype (Sym2 α)`.
-/
instance instDecidableRel [DecidableEq α] : DecidableRel (Rel α) := fun _ _ => decidable_of_iff' _ rel_iff

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