decidablePiFintype — Mathlib

English

There is a decidable equality on the type of equivalences α ≃ β, given [DecidableEq β] and [Fintype α].

Русский

Существует разрешимое равенство на множество эквивалентностей α ≃ β при данных [DecidableEq β] и [Fintype α].

LaTeX

$$$$ \forall {\alpha \beta}, [\DecidableEq \beta] \rightarrow [\mathrm{Fintype} \alpha] \rightarrow \DecidableEq (\alpha \simeq \beta) $$$$

Lean4

instance decidablePiFintype {α} {β : α → Type*} [∀ a, DecidableEq (β a)] [Fintype α] : DecidableEq (∀ a, β a) :=
  fun f g => decidable_of_iff (∀ a ∈ @univ α _, f a = g a) (by simp [funext_iff])

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