@[inline]

def Function.curry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} : (α × β → φ) → α → β → φ

Transforms a function from pairs into an equivalent two-parameter function.

Examples:

• Function.curry (fun (x, y) => x + y) 3 5 = 8
• Function.curry Prod.swap 3 "five" = ("five", 3)

Equations

• Function.curry f a b = f (a, b)

@[inline]

def Function.uncurry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} : (α → β → φ) → α × β → φ

Transforms a two-parameter function into an equivalent function from pairs.

Examples:

• Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]
• [("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]

Equations

• Function.uncurry f a = f a.fst a.snd

@[simp]

theorem Function.curry_uncurry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (f : α → β → φ) : curry (uncurry f) = f

@[simp]

theorem Function.uncurry_curry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (f : α × β → φ) : uncurry (curry f) = f

@[simp]

theorem Function.uncurry_apply_pair {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) (x : α) (y : β) : uncurry f (x, y) = f x y

@[simp]

theorem Function.curry_apply {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ) (x : α) (y : β) : curry f x y = f (x, y)

def Function.Injective {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

A function f : α → β is called injective if f x = f y implies x = y.

Equations

• Function.Injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂

theorem Function.Injective.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} {f : α → β} (hg : Injective g) (hf : Injective f) : Injective (g ∘ f)

def Function.Surjective {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

A function f : α → β is called surjective if every b : β is equal to f a for some a : α.

Equations

• Function.Surjective f = ∀ (b : β), ∃ (a : α), f a = b

theorem Function.Surjective.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} {f : α → β} (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f)

@[implicit_reducible]

def Function.LeftInverse {α : Sort u_1} {β : Sort u_2} (g : β → α) (f : α → β) : Prop

LeftInverse g f means that g is a left inverse to f. That is, g ∘ f = id.

Equations

• Function.LeftInverse g f = ∀ (x : α), g (f x) = x

def Function.HasLeftInverse {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

HasLeftInverse f means that f has an unspecified left inverse.

Equations

• Function.HasLeftInverse f = ∃ (finv : β → α), Function.LeftInverse finv f

@[implicit_reducible]

def Function.RightInverse {α : Sort u_1} {β : Sort u_2} (g : β → α) (f : α → β) : Prop

RightInverse g f means that g is a right inverse to f. That is, f ∘ g = id.

Equations

• Function.RightInverse g f = Function.LeftInverse f g

def Function.HasRightInverse {α : Sort u_1} {β : Sort u_2} (f : α → β) : Prop

HasRightInverse f means that f has an unspecified right inverse.

Equations

• Function.HasRightInverse f = ∃ (finv : β → α), Function.RightInverse finv f

theorem Function.LeftInverse.injective {α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β} : LeftInverse g f → Injective f

theorem Function.HasLeftInverse.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} : HasLeftInverse f → Injective f

theorem Function.rightInverse_of_injective_of_leftInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (injf : Injective f) (lfg : LeftInverse f g) : RightInverse f g

theorem Function.RightInverse.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : RightInverse g f) : Surjective f

theorem Function.HasRightInverse.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} : HasRightInverse f → Surjective f

theorem Function.leftInverse_of_surjective_of_rightInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (surjf : Surjective f) (rfg : RightInverse f g) : LeftInverse f g

theorem Function.injective_id {α : Sort u_1} : Injective id

theorem Function.surjective_id {α : Sort u_1} : Surjective id

theorem Function.Injective.eq_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : Injective f) {a b : α} : f a = f b ↔ a = b

theorem Function.Injective.eq_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : Injective f) {a b : α} {c : β} (h : f b = c) : f a = c ↔ a = b

theorem Function.Injective.ne {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Injective f) {a₁ a₂ : α} : a₁ ≠ a₂ → f a₁ ≠ f a₂

theorem Function.Injective.ne_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Injective f) {x y : α} : f x ≠ f y ↔ x ≠ y

theorem Function.Injective.ne_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Injective f) {x y : α} {z : β} (h : f y = z) : f x ≠ z ↔ x ≠ y

theorem Function.LeftInverse.id {α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β} (h : LeftInverse g f) : g ∘ f = id

theorem Function.RightInverse.id {α : Sort u_1} {β : Sort u_2} {g : β → α} {f : α → β} (h : RightInverse g f) : f ∘ g = id

theorem Function.Injective.exists_leftInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Injective f) [hα : Nonempty α] : ∃ (g : β → α), LeftInverse g f

@[deprecated Function.Injective.exists_leftInverse (since := "2026-07-06")]

theorem Function.Injective.leftInverse {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : Injective f) [hα : Nonempty α] : ∃ (g : β → α), LeftInverse g f