decidableBijectiveFintype — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance decidableBijectiveFintype [DecidableEq β] [Fintype α] [Fintype β] :
    DecidablePred (Bijective : (α → β) → Prop) := fun x => by unfold Bijective; infer_instance

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