Theorems · Definition · combinatorics

Function.Injective.invOfMemRange

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

The inverse of an hf : injective function f : α → β, of the type ↥(Set.range f) → α. This is the computable version of Function.invFun that requires Fintype α and DecidableEq β, or the function version of applying (Equiv.ofInjective f hf).symm. This function should not usually be used for actual computation because for most cases, an explicit inverse can be stated that has better computational properties. This function computes by checking all terms a : α to find the f a = b, so it is O(N) where N = Fintype.card α.

Defined in

Mathlib.Data.Fintype.Inv

Cited by

6 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq