# mathlibdocumentation

logic.function.basic

# Miscellaneous function constructions and lemmas #

@[reducible]
def function.eval {α : Sort u_1} {β : α → Sort u_2} (x : α) (f : Π (x : α), β x) :
β x

Evaluate a function at an argument. Useful if you want to talk about the partially applied function.eval x : (Π x, β x) → β x.

Equations
• = f x
@[simp]
theorem function.eval_apply {α : Sort u_1} {β : α → Sort u_2} (x : α) (f : Π (x : α), β x) :
= f x
theorem function.comp_apply {α : Sort u} {β : Sort v} {φ : Sort w} (f : β → φ) (g : α → β) (a : α) :
(f g) a = f (g a)
theorem function.const_def {α : Sort u_1} {β : Sort u_2} {y : β} :
(λ (x : α), y) =
@[simp]
theorem function.const_apply {α : Sort u_1} {β : Sort u_2} {y : β} {x : α} :
x = y
@[simp]
theorem function.const_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {c : γ} :
f =
@[simp]
theorem function.comp_const {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : β → γ} {b : β} :
f = (f b)
theorem function.const_injective {α : Sort u_1} {β : Sort u_2} [nonempty α] :
@[simp]
theorem function.const_inj {α : Sort u_1} {β : Sort u_2} [nonempty α] {y₁ y₂ : β} :
y₁ = y₂ y₁ = y₂
theorem function.id_def {α : Sort u_1} :
id = λ (x : α), x
@[ext]
theorem function.hfunext {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : Π (a : α), β a} {f' : Π (a : α'), β' a} (hα : α = α') (h : ∀ (a : α) (a' : α'), a == a'f a == f' a') :
f == f'
theorem function.funext_iff {α : Sort u_1} {β : α → Sort u_2} {f₁ f₂ : Π (x : α), β x} :
f₁ = f₂ ∀ (a : α), f₁ a = f₂ a
theorem function.ne_iff {α : Sort u_1} {β : α → Sort u_2} {f₁ f₂ : Π (a : α), β a} :
f₁ f₂ ∃ (a : α), f₁ a f₂ a
@[protected]
theorem function.bijective.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.bijective f) :
@[protected]
theorem function.bijective.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.bijective f) :
theorem function.injective.eq_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : function.injective f) {a b : α} :
f a = f b a = b
theorem function.injective.eq_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : function.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 : function.injective f) {a₁ a₂ : α} :
a₁ a₂f a₁ f a₂
theorem function.injective.ne_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.injective f) {x y : α} :
f x f y x y
theorem function.injective.ne_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.injective f) {x y : α} {z : β} (h : f y = z) :
f x z x y
@[protected]
def function.injective.decidable_eq {α : Sort u_1} {β : Sort u_2} {f : α → β} [decidable_eq β] (I : function.injective f) :

If the co-domain β of an injective function f : α → β has decidable equality, then the domain α also has decidable equality.

Equations
theorem function.injective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (I : function.injective (f g)) :
theorem function.injective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.injective f) (g : γ → α) :
theorem function.injective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : function.bijective g) :
theorem function.injective.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} (hg : function.injective g) :

Composition by an injective function on the left is itself injective.

theorem function.injective_of_subsingleton {α : Sort u_1} {β : Sort u_2} [subsingleton α] (f : α → β) :
theorem function.injective.dite {α : Sort u_1} {β : Sort u_2} (p : α → Prop) {f : {a // p a} → β} {f' : {a // ¬p a} → β} (hf : function.injective f) (hf' : function.injective f') (im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f x, hx⟩ f' x', hx'⟩) :
function.injective (λ (x : α), dite (p x) (λ (h : p x), f x, h⟩) (λ (h : ¬p x), f' x, h⟩))
theorem function.surjective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (S : function.surjective (f g)) :
theorem function.surjective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : function.surjective g) :
theorem function.surjective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.bijective f) (g : γ → α) :
@[protected, instance]
def function.decidable_eq_pfun (p : Prop) [decidable p] (α : p → Type u_1) [Π (hp : p), decidable_eq (α hp)] :
decidable_eq (Π (hp : p), α hp)
Equations
@[protected]
theorem function.surjective.forall {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → Prop} :
(∀ (y : β), p y) ∀ (x : α), p (f x)
@[protected]
theorem function.surjective.forall₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → β → Prop} :
(∀ (y₁ y₂ : β), p y₁ y₂) ∀ (x₁ x₂ : α), p (f x₁) (f x₂)
@[protected]
theorem function.surjective.forall₃ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → β → β → Prop} :
(∀ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ∀ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
@[protected]
theorem function.surjective.exists {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → Prop} :
(∃ (y : β), p y) ∃ (x : α), p (f x)
@[protected]
theorem function.surjective.exists₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → β → Prop} :
(∃ (y₁ y₂ : β), p y₁ y₂) ∃ (x₁ x₂ : α), p (f x₁) (f x₂)
@[protected]
theorem function.surjective.exists₃ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → β → β → Prop} :
(∃ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ∃ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
theorem function.surjective.injective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.surjective f) :
function.injective (λ (g : β → γ), g f)
@[protected]
theorem function.surjective.right_cancellable {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.surjective f) {g₁ g₂ : β → γ} :
g₁ f = g₂ f g₁ = g₂
theorem function.surjective_of_right_cancellable_Prop {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : ∀ (g₁ g₂ : β → Prop), g₁ f = g₂ fg₁ = g₂) :
theorem function.bijective_iff_exists_unique {α : Sort u_1} {β : Sort u_2} (f : α → β) :
∀ (b : β), ∃! (a : α), f a = b
@[protected]
theorem function.bijective.exists_unique {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.bijective f) (b : β) :
∃! (a : α), f a = b

Shorthand for using projection notation with function.bijective_iff_exists_unique.

theorem function.bijective.exists_unique_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.bijective f) {p : β → Prop} :
(∃! (y : β), p y) ∃! (x : α), p (f x)
theorem function.bijective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : function.bijective g) :
theorem function.bijective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.bijective f) (g : γ → α) :
theorem function.cantor_surjective {α : Type u_1} (f : α → set α) :

Cantor's diagonal argument implies that there are no surjective functions from α to set α.

theorem function.cantor_injective {α : Type u_1} (f : set α → α) :

Cantor's diagonal argument implies that there are no injective functions from set α to α.

theorem function.not_surjective_Type {α : Type u} (f : α → Type (max u v)) :

There is no surjection from α : Type u into Type u. This theorem demonstrates why Type : Type would be inconsistent in Lean.

def function.is_partial_inv {α : Type u_1} {β : Sort u_2} (f : α → β) (g : β → ) :
Prop

g is a partial inverse to f (an injective but not necessarily surjective function) if g y = some x implies f x = y, and g y = none implies that y is not in the range of f.

Equations
• = ∀ (x : α) (y : β), g y = f x = y
theorem function.is_partial_inv_left {α : Type u_1} {β : Sort u_2} {f : α → β} {g : β → } (H : g) (x : α) :
g (f x) =
theorem function.injective_of_partial_inv {α : Type u_1} {β : Sort u_2} {f : α → β} {g : β → } (H : g) :
theorem function.injective_of_partial_inv_right {α : Type u_1} {β : Sort u_2} {f : α → β} {g : β → } (H : g) (x y : β) (b : α) (h₁ : b g x) (h₂ : b g y) :
x = y
theorem function.left_inverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : g) :
f g = id
theorem function.left_inverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
f g = id
theorem function.right_inverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : g) :
g f = id
theorem function.right_inverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
g f = id
theorem function.left_inverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : g) (hh : i) :
theorem function.right_inverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : g) (hh : i) :
theorem function.left_inverse.right_inverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : f) :
theorem function.right_inverse.left_inverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : f) :
theorem function.left_inverse.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : g) :
theorem function.right_inverse.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : g) :
theorem function.left_inverse.right_inverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : g) (hf : function.injective f) :
theorem function.left_inverse.right_inverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : g) (hg : function.surjective g) :
theorem function.right_inverse.left_inverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
theorem function.right_inverse.left_inverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
theorem function.left_inverse.eq_right_inverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g₁ g₂ : β → α} (h₁ : f) (h₂ : f) :
g₁ = g₂
noncomputable def function.partial_inv {α : Type u_1} {β : Sort u_2} (f : α → β) (b : β) :

We can use choice to construct explicitly a partial inverse for a given injective function f.

Equations
• = dite (∃ (a : α), f a = b) (λ (h : ∃ (a : α), f a = b), (λ (h : ¬∃ (a : α), f a = b), option.none)
theorem function.partial_inv_of_injective {α : Type u_1} {β : Sort u_2} {f : α → β} (I : function.injective f) :
theorem function.partial_inv_left {α : Type u_1} {β : Sort u_2} {f : α → β} (I : function.injective f) (x : α) :
(f x) =
noncomputable def function.inv_fun {α : Sort u_1} {β : Sort u_2} [nonempty α] (f : α → β) :
β → α

The inverse of a function (which is a left inverse if f is injective and a right inverse if f is surjective).

Equations
• = λ (y : β), dite (∃ (x : α), f x = y) (λ (h : ∃ (x : α), f x = y), h.some) (λ (h : ¬∃ (x : α), f x = y),
theorem function.inv_fun_eq {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} {b : β} (h : ∃ (a : α), f a = b) :
f b) = b
theorem function.inv_fun_neg {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} {b : β} (h : ¬∃ (a : α), f a = b) :
theorem function.inv_fun_eq_of_injective_of_right_inverse {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} {g : β → α} (hf : function.injective f) (hg : f) :
theorem function.right_inverse_inv_fun {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} (hf : function.surjective f) :
theorem function.left_inverse_inv_fun {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} (hf : function.injective f) :
theorem function.inv_fun_surjective {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} (hf : function.injective f) :
theorem function.inv_fun_comp {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} (hf : function.injective f) :
= id
theorem function.injective.has_left_inverse {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} (hf : function.injective f) :
theorem function.injective_iff_has_left_inverse {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α → β} :
noncomputable def function.surj_inv {α : Sort u} {β : Sort v} {f : α → β} (h : function.surjective f) (b : β) :
α

The inverse of a surjective function. (Unlike inv_fun, this does not require α to be inhabited.)

Equations
theorem function.surj_inv_eq {α : Sort u} {β : Sort v} {f : α → β} (h : function.surjective f) (b : β) :
f b) = b
theorem function.right_inverse_surj_inv {α : Sort u} {β : Sort v} {f : α → β} (hf : function.surjective f) :
theorem function.left_inverse_surj_inv {α : Sort u} {β : Sort v} {f : α → β} (hf : function.bijective f) :
theorem function.surjective.has_right_inverse {α : Sort u} {β : Sort v} {f : α → β} (hf : function.surjective f) :
theorem function.surjective_iff_has_right_inverse {α : Sort u} {β : Sort v} {f : α → β} :
theorem function.bijective_iff_has_inverse {α : Sort u} {β : Sort v} {f : α → β} :
∃ (g : β → α),
theorem function.injective_surj_inv {α : Sort u} {β : Sort v} {f : α → β} (h : function.surjective f) :
theorem function.surjective_to_subsingleton {α : Sort u} {β : Sort v} [na : nonempty α] [subsingleton β] (f : α → β) :
theorem function.surjective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ} (hg : function.surjective g) :

Composition by an surjective function on the left is itself surjective.

theorem function.bijective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ} (hg : function.bijective g) :

Composition by an bijective function on the left is itself bijective.

def function.update {α : Sort u} {β : α → Sort v} [decidable_eq α] (f : Π (a : α), β a) (a' : α) (v : β a') (a : α) :
β a

Replacing the value of a function at a given point by a given value.

Equations
• a' v a = dite (a = a') (λ (h : a = a'), eq.rec v _) (λ (h : ¬a = a'), f a)
theorem function.update_apply {α : Sort u} [decidable_eq α] {β : Sort u_1} (f : α → β) (a' : α) (b : β) (a : α) :
a' b a = ite (a = a') b (f a)

On non-dependent functions, function.update can be expressed as an ite

@[simp]
theorem function.update_same {α : Sort u} {β : α → Sort v} [decidable_eq α] (a : α) (v : β a) (f : Π (a : α), β a) :
v a = v
theorem function.surjective_eval {α : Sort u} {β : α → Sort v} [h : ∀ (a : α), nonempty (β a)] (a : α) :
theorem function.update_injective {α : Sort u} {β : α → Sort v} [decidable_eq α] (f : Π (a : α), β a) (a' : α) :
@[simp]
theorem function.update_noteq {α : Sort u} {β : α → Sort v} [decidable_eq α] {a a' : α} (h : a a') (v : β a') (f : Π (a : α), β a) :
a' v a = f a
theorem function.forall_update_iff {α : Sort u} {β : α → Sort v} [decidable_eq α] (f : Π (a : α), β a) {a : α} {b : β a} (p : Π (a : α), β a → Prop) :
(∀ (x : α), p x a b x)) p a b ∀ (x : α), x ap x (f x)
theorem function.exists_update_iff {α : Sort u} {β : α → Sort v} [decidable_eq α] (f : Π (a : α), β a) {a : α} {b : β a} (p : Π (a : α), β a → Prop) :
(∃ (x : α), p x a b x)) p a b ∃ (x : α) (H : x a), p x (f x)
theorem function.update_eq_iff {α : Sort u} {β : α → Sort v} [decidable_eq α] {a : α} {b : β a} {f g : Π (a : α), β a} :
b = g b = g a ∀ (x : α), x af x = g x
theorem function.eq_update_iff {α : Sort u} {β : α → Sort v} [decidable_eq α] {a : α} {b : β a} {f g : Π (a : α), β a} :
g = b g a = b ∀ (x : α), x ag x = f x
@[simp]
theorem function.update_eq_self {α : Sort u} {β : α → Sort v} [decidable_eq α] (a : α) (f : Π (a : α), β a) :
(f a) = f
theorem function.update_comp_eq_of_forall_ne' {α : Sort u} {β : α → Sort v} [decidable_eq α] {α' : Sort u_1} (g : Π (a : α), β a) {f : α' → α} {i : α} (a : β i) (h : ∀ (x : α'), f x i) :
(λ (j : α'), a (f j)) = λ (j : α'), g (f j)
theorem function.update_comp_eq_of_forall_ne {α' : Sort w} [decidable_eq α'] {α : Sort u_1} {β : Sort u_2} (g : α' → β) {f : α → α'} {i : α'} (a : β) (h : ∀ (x : α), f x i) :
a f = g f

Non-dependent version of function.update_comp_eq_of_forall_ne'

theorem function.update_comp_eq_of_injective' {α : Sort u} {β : α → Sort v} {α' : Sort w} [decidable_eq α] [decidable_eq α'] (g : Π (a : α), β a) {f : α' → α} (hf : function.injective f) (i : α') (a : β (f i)) :
(λ (j : α'), (f i) a (f j)) = function.update (λ (i : α'), g (f i)) i a
theorem function.update_comp_eq_of_injective {α : Sort u} {α' : Sort w} [decidable_eq α] [decidable_eq α'] {β : Sort u_1} (g : α' → β) {f : α → α'} (hf : function.injective f) (i : α) (a : β) :
(f i) a f = function.update (g f) i a

Non-dependent version of function.update_comp_eq_of_injective'

theorem function.apply_update {ι : Sort u_1} [decidable_eq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} (f : Π (i : ι), α iβ i) (g : Π (i : ι), α i) (i : ι) (v : α i) (j : ι) :
f j i v j) = function.update (λ (k : ι), f k (g k)) i (f i v) j
theorem function.apply_update₂ {ι : Sort u_1} [decidable_eq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} {γ : ι → Sort u_4} (f : Π (i : ι), α iβ iγ i) (g : Π (i : ι), α i) (h : Π (i : ι), β i) (i : ι) (v : α i) (w : β i) (j : ι) :
f j i v j) i w j) = function.update (λ (k : ι), f k (g k) (h k)) i (f i v w) j
theorem function.comp_update {α : Sort u} [decidable_eq α] {α' : Sort u_1} {β : Sort u_2} (f : α' → β) (g : α → α') (i : α) (v : α') :
f v = function.update (f g) i (f v)
theorem function.update_comm {α : Sort u_1} [decidable_eq α] {β : α → Sort u_2} {a b : α} (h : a b) (v : β a) (w : β b) (f : Π (a : α), β a) :
@[simp]
theorem function.update_idem {α : Sort u_1} [decidable_eq α] {β : α → Sort u_2} {a : α} (v w : β a) (f : Π (a : α), β a) :
function.update a v) a w = w
noncomputable def function.extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (e' : β → γ) :
β → γ

extend f g e' extends a function g : α → γ along a function f : α → β to a function β → γ, by using the values of g on the range of f and the values of an auxiliary function e' : β → γ elsewhere.

Mostly useful when f is injective.

Equations
• e' = λ (b : β), dite (∃ (a : α), f a = b) (λ (h : ∃ (a : α), f a = b), g (classical.some h)) (λ (h : ¬∃ (a : α), f a = b), e' b)
theorem function.extend_def {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [decidable (∃ (a : α), f a = b)] :
e' b = dite (∃ (a : α), f a = b) (λ (h : ∃ (a : α), f a = b), g (classical.some h)) (λ (h : ¬∃ (a : α), f a = b), e' b)
@[simp]
theorem function.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.injective f) (g : α → γ) (e' : β → γ) (a : α) :
e' (f a) = g a
@[simp]
theorem function.extend_apply' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (g : α → γ) (e' : β → γ) (b : β) (hb : ¬∃ (a : α), f a = b) :
e' b = e' b
theorem function.apply_extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {δ : Sort u_4} (hf : function.injective f) (F : γ → δ) (g : α → γ) (e' : β → γ) (b : β) :
F g e' b) = (F g) (F e') b
theorem function.extend_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.injective f) (e' : β → γ) :
function.injective (λ (g : α → γ), e')
@[simp]
theorem function.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.injective f) (g : α → γ) (e' : β → γ) :
e' f = g
theorem function.injective.surjective_comp_right' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.injective f) (g₀ : β → γ) :
function.surjective (λ (g : β → γ), g f)
theorem function.injective.surjective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} [nonempty γ] (hf : function.injective f) :
function.surjective (λ (g : β → γ), g f)
theorem function.bijective.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.bijective f) :
function.bijective (λ (g : β → γ), g f)
theorem function.uncurry_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) :
= λ (p : α × β), f p.fst p.snd
@[simp]
theorem function.uncurry_apply_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : α) (y : β) :
(x, y) = f x y
@[simp]
theorem function.curry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α × β → γ) (x : α) (y : β) :
y = f (x, y)
def function.bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : γ → δ → ε) (g : α → γ) (h : β → δ) (a : α) (b : β) :
ε

Compose a binary function f with a pair of unary functions g and h. If both arguments of f have the same type and g = h, then bicompl f g g = f on g.

Equations
• h a b = f (g a) (h b)
Instances for function.bicompl
def function.bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : γ → δ) (g : α → β → γ) (a : α) (b : β) :
δ

Compose an unary function f with a binary function g.

Equations
• a b = f (g a b)
Instances for function.bicompr
theorem function.uncurry_bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ) (g : γ → δ) :
theorem function.uncurry_bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : γ → δ → ε) (g : α → γ) (h : β → δ) :
@[class]
structure function.has_uncurry (α : Type u_5) (β : out_param (Type u_6)) (γ : out_param (Type u_7)) :
Type (max u_5 u_6 u_7)
• uncurry : α → β → γ

Records a way to turn an element of α into a function from β to γ. The most generic use is to recursively uncurry. For instance f : α → β → γ → δ will be turned into ↿f : α × β × γ → δ. One can also add instances for bundled maps.

Instances of this typeclass
Instances of other typeclasses for function.has_uncurry
• function.has_uncurry.has_sizeof_inst
@[protected, instance]
def function.has_uncurry_base {α : Type u_1} {β : Type u_2} :
function.has_uncurry (α → β) α β
Equations
@[protected, instance]
def function.has_uncurry_induction {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [ δ] :
function.has_uncurry (α → β) × γ) δ
Equations
def function.involutive {α : Sort u_1} (f : α → α) :
Prop

A function is involutive, if f ∘ f = id.

Equations
• = ∀ (x : α), f (f x) = x
theorem function.involutive_iff_iter_2_eq_id {α : Sort u_1} {f : α → α} :
@[simp]
theorem function.involutive.comp_self {α : Sort u} {f : α → α} (h : function.involutive f) :
f f = id
@[protected]
theorem function.involutive.left_inverse {α : Sort u} {f : α → α} (h : function.involutive f) :
@[protected]
theorem function.involutive.right_inverse {α : Sort u} {f : α → α} (h : function.involutive f) :
@[protected]
theorem function.involutive.injective {α : Sort u} {f : α → α} (h : function.involutive f) :
@[protected]
theorem function.involutive.surjective {α : Sort u} {f : α → α} (h : function.involutive f) :
@[protected]
theorem function.involutive.bijective {α : Sort u} {f : α → α} (h : function.involutive f) :
@[protected]
theorem function.involutive.ite_not {α : Sort u} {f : α → α} (h : function.involutive f) (P : Prop) [decidable P] (x : α) :
f (ite P x (f x)) = ite (¬P) x (f x)

Involuting an ite of an involuted value x : α negates the Prop condition in the ite.

@[protected]
theorem function.involutive.eq_iff {α : Sort u} {f : α → α} (h : function.involutive f) {x y : α} :
f x = y x = f y

An involution commutes across an equality. Compare to function.injective.eq_iff.

def function.injective2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) :
Prop

The property of a binary function f : α → β → γ being injective. Mathematically this should be thought of as the corresponding function α × β → γ being injective.

Equations
• = ∀ ⦃a₁ a₂ : α⦄ ⦃b₁ b₂ : β⦄, f a₁ b₁ = f a₂ b₂a₁ = a₂ b₁ = b₂
@[protected]
theorem function.injective2.left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : function.injective2 f) (b : β) :
function.injective (λ (a : α), f a b)

A binary injective function is injective when only the left argument varies.

@[protected]
theorem function.injective2.right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : function.injective2 f) (a : α) :

A binary injective function is injective when only the right argument varies.

@[protected]
theorem function.injective2.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} (hf : function.injective2 f) :
theorem function.injective2.left' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : function.injective2 f) [nonempty β] :

As a map from the left argument to a unary function, f is injective.

theorem function.injective2.right' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : function.injective2 f) [nonempty α] :
function.injective (λ (b : β) (a : α), f a b)

As a map from the right argument to a unary function, f is injective.

theorem function.injective2.eq_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : function.injective2 f) {a₁ a₂ : α} {b₁ b₂ : β} :
f a₁ b₁ = f a₂ b₂ a₁ = a₂ b₁ = b₂
noncomputable def function.sometimes {α : Sort u_1} {β : Sort u_2} [nonempty β] (f : α → β) :
β

sometimes f evaluates to some value of f, if it exists. This function is especially interesting in the case where α is a proposition, in which case f is necessarily a constant function, so that sometimes f = f a for all a.

Equations
theorem function.sometimes_eq {p : Prop} {α : Sort u_1} [nonempty α] (f : p → α) (a : p) :
= f a
theorem function.sometimes_spec {p : Prop} {α : Sort u_1} [nonempty α] (P : α → Prop) (f : p → α) (a : p) (h : P (f a)) :
P
def set.piecewise {α : Type u} {β : α → Sort v} (s : set α) (f g : Π (i : α), β i) [Π (j : α), decidable (j s)] (i : α) :
β i

s.piecewise f g is the function equal to f on the set s, and to g on its complement.

Equations

### Bijectivity of eq.rec, eq.mp, eq.mpr, and cast#

theorem eq_rec_on_bijective {α : Sort u_1} {C : α → Sort u_2} {a a' : α} (h : a = a') :
theorem eq_mp_bijective {α β : Sort u_1} (h : α = β) :
theorem eq_mpr_bijective {α β : Sort u_1} (h : α = β) :
theorem cast_bijective {α β : Sort u_1} (h : α = β) :

Note these lemmas apply to Type* not Sort*, as the latter interferes with simp, and is trivial anyway.

@[simp]
theorem eq_rec_inj {α : Sort u_1} {a a' : α} (h : a = a') {C : α → Type u_2} (x y : C a) :
eq.rec x h = eq.rec y h x = y
@[simp]
theorem cast_inj {α β : Type u_1} (h : α = β) {x y : α} :
cast h x = cast h y x = y
theorem function.left_inverse.eq_rec_eq {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : f) (C : Π (a : α), γ (f a)) (a : α) :
eq.rec (C (g (f a))) _ = C a
theorem function.left_inverse.eq_rec_on_eq {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : f) (C : Π (a : α), γ (f a)) (a : α) :
_.rec_on (C (g (f a))) = C a
theorem function.left_inverse.cast_eq {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : f) (C : Π (a : α), γ (f a)) (a : α) :
cast _ (C (g (f a))) = C a
def set.separates_points {α : Type u_1} {β : Type u_2} (A : set (α → β)) :
Prop

A set of functions "separates points" if for each pair of distinct points there is a function taking different values on them.

Equations
theorem is_symm_op.flip_eq {α : Type u_1} {β : out_param (Type u_2)} (op : α → α → β) [ β op] :
flip op = op
theorem inv_image.equivalence {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (h : equivalence r) :