decidableEqEmbeddingFintype — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance decidableEqEmbeddingFintype [DecidableEq β] [Fintype α] : DecidableEq (α ↪ β) := fun a b =>
  decidable_of_iff ((a : α → β) = b) Function.Embedding.coe_injective.eq_iff

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