Theorems · Definition · combinatorics

Function.Embedding.toEquivRange

{α : Type u_1} → {β : Type u_2} → [Fintype α] → [DecidableEq β] → (f : α ↪ β) → α ≃ ↑(Set.range ⇑f)

Computably turn an embedding f : α ↪ β into an equiv α ≃ Set.range f, if α is a Fintype. Has poor computational performance, due to exhaustive searching in constructed inverse. When a better inverse is known, use Equiv.ofLeftInverse' or Equiv.ofLeftInverse instead. This is the computable version of Equiv.ofInjective.

Defined in

Mathlib.Logic.Equiv.Fintype

Cited by

23 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEq