instDecidableRelVectorEquivOfDecidableEq

English

If α has decidable equality, then the relation ‘vector x ≈ vector y’ (permutation equivalence) on Vector α n is decidable.

Русский

Если на α задано конечное равенство, то отношение эквивалентности векторов по перестановке решений осуществимо.

LaTeX

$$$\\forall (α) (n) [\\mathrm{DecidableEq}(α)],\\; \\text{DecidableRel}(\\,x,y: \\mathrm{List.Vector} \\; α\\; n\\,\\;\\mapsto\\; \\text{Perm}(x,y))$$$

Lean4

instance {α : Type*} {n : ℕ} [DecidableEq α] : DecidableRel (· ≈ · : List.Vector α n → List.Vector α n → Prop) :=
  fun _ _ => List.decidablePerm _ _

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