decidableEqPiFinset — Mathlib

English

If for every a in s, β(a) has decidable equality, then the dependent function type ∀ a ∈ s, β(a) has decidable equality.

Русский

Если для каждого элемента a из s множество β(a) имеет разрешимое равенство, то производное множество функций ∀ a ∈ s, β(a) имеет разрешимое равенство.

LaTeX

$$$\\bigl(\\forall a\\in s,\\ DecidableEq(β(a))\\bigr) \\Rightarrow DecidableEq(\\forall a\\in s,\\, β(a))$$$

Lean4

/-- decidable equality for functions whose domain is bounded by finsets -/
instance decidableEqPiFinset {β : α → Type*} [_h : ∀ a, DecidableEq (β a)] : DecidableEq (∀ a ∈ s, β a) :=
  Multiset.decidableEqPiMultiset

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