Theorems · Definition · order theory

Function.invFunOn

{α : Type u_1} → {β : Type u_2} → [Nonempty α] → (α → β) → Set α → β → α

Construct the inverse for a function f on domain s. This function is a right inverse of f on f '' s. For a computable version, see Function.Embedding.invOfMemRange.

Defined in

Mathlib.Data.Set.Function

Cited by

35 results in Mathlib

Foundations

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

Assumes

Nonempty