decidableInjectiveFintype — Mathlib

English

There is a decidable predicate Injective for functions α → β given [DecidableEq β] and [Fintype α].

Русский

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

LaTeX

$$$$ \text{DecidablePred}(\mathrm{Injective} : (\alpha \to \beta) \to \mathrm{Prop}) $$$$

Lean4

instance decidableInjectiveFintype [DecidableEq β] [Fintype α] : DecidablePred (Injective : (α → β) → Prop) :=
  -- Use custom implementation for better performance.
   fun f => decidable_of_iff ((Multiset.map f univ.val).Nodup) nodup_map_univ_iff_injective

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