# mathlibdocumentation

logic.function.basic

# Miscellaneous function constructions and lemmas

def function.eval {α : Sort u_1} {β : α → Sort u_2} (x : α) :
(Π (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)

@[ext]
theorem function.hfunext {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : Π (a : α), β a} {f' : Π (a : α'), β' a} :
α = α'(∀ (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

@[simp]
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 : β} :
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 : β} :
f y = z(f x z x y)

def function.injective.decidable_eq {α : Sort u_1} {β : Sort u_2} {f : α → β} [decidable_eq β] :

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 : γ → α} :

theorem function.surjective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} :

@[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
theorem function.surjective.forall {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → Prop} :
(∀ (y : β), p y) ∀ (x : α), p (f x)

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₂)

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₃)

theorem function.surjective.exists {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → Prop} :
(∃ (y : β), p y) ∃ (x : α), p (f x)

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₂)

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.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 α.

def function.is_partial_inv {α : Type u_1} {β : Sort u_2} :
(α → β)(β → option α) → 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 = some x f x = y
theorem function.is_partial_inv_left {α : Type u_1} {β : Sort u_2} {f : α → β} {g : β → } (H : g) (x : α) :
g (f x) = some x

theorem function.injective_of_partial_inv {α : Type u_1} {β : Sort u_2} {f : α → β} {g : β → } :

theorem function.injective_of_partial_inv_right {α : Type u_1} {β : Sort u_2} {f : α → β} {g : β → } (H : g) (x y : β) (b : α) :
b g xb g yx = y

theorem function.left_inverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α → β} {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 : β → α} :
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 : γ → β} :
function.left_inverse (h f) (g i)

theorem function.right_inverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} :
function.right_inverse (h f) (g i)

theorem function.left_inverse.right_inverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :

theorem function.right_inverse.left_inverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :

theorem function.left_inverse.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :

theorem function.right_inverse.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₂ : β → α} :
g₁ = g₂

def function.partial_inv {α : Type u_1} {β : Sort u_2} :
(α → β)β →

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

Equations
theorem function.partial_inv_of_injective {α : Type u_1} {β : Sort u_2} {f : α → β} :

theorem function.partial_inv_left {α : Type u_1} {β : Sort u_2} {f : α → β} (I : function.injective f) (x : α) :
(f x) = some x

def function.inv_fun_on {α : Type u} [n : nonempty α] {β : Sort v} :
(α → β)set αβ → α

Construct the inverse for a function f on domain s. This function is a right inverse of f on f '' s.

Equations
theorem function.inv_fun_on_pos {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {b : β} :
(∃ (a : α) (H : a s), f a = b) b s f b) = b

theorem function.inv_fun_on_mem {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {b : β} :
(∃ (a : α) (H : a s), f a = b) b s

theorem function.inv_fun_on_eq {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {b : β} :
(∃ (a : α) (H : a s), f a = b)f b) = b

theorem function.inv_fun_on_eq' {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {a : α} :
(∀ (x : α), x s∀ (y : α), y sf x = f yx = y)a s (f a) = a

theorem function.inv_fun_on_neg {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {b : β} :
(¬∃ (a : α) (H : a s), f a = b)

def function.inv_fun {α : Type u} [n : nonempty α] {β : Sort v} :
(α → β)β → α

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

Equations
theorem function.inv_fun_eq {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {b : β} :
(∃ (a : α), f a = b)f b) = b

theorem function.inv_fun_neg {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {b : β} :
(¬∃ (a : α), f a = b)

theorem function.inv_fun_eq_of_injective_of_right_inverse {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {g : β → α} :

theorem function.right_inverse_inv_fun {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} :

theorem function.left_inverse_inv_fun {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} :

theorem function.inv_fun_surjective {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} :

theorem function.inv_fun_comp {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} :
= id

theorem function.injective.has_left_inverse {α : Type u} [i : nonempty α] {β : Sort v} {f : α → β} :

theorem function.injective_iff_has_left_inverse {α : Type u} [i : nonempty α] {β : Sort v} {f : α → β} :

def function.surj_inv {α : Sort u} {β : Sort v} {f : α → β} :
β → α

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 : α → β} :

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) :

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)
@[simp]
theorem function.update_same {α : Sort u} {β : α → Sort v} [decidable_eq α] (a : α) (v : β a) (f : Π (a : α), β a) :
v a = v

@[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

@[simp]
theorem function.update_eq_self {α : Sort u} {β : α → Sort v} [decidable_eq α] (a : α) (f : Π (a : α), β a) :
(f a) = f

theorem function.update_comp {α : Sort u} {α' : Sort w} [decidable_eq α] [decidable_eq α'] {β : Sort v} (f : α → β) {g : α' → α} (hg : function.injective g) (a : α') (v : β) :
(g a) v g = function.update (f g) a v

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.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

def function.extend {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α → β)(α → γ)(β → γ)β → γ

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 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (e' : β → γ) (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 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} (hf : function.injective f) (g : α → γ) (e' : β → γ) (a : α) :
e' (f a) = g a

@[simp]
theorem function.extend_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} (hf : function.injective f) (g : α → γ) (e' : β → γ) :
e' f = g

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} :
(γ → δ → ε)(α → γ)(β → δ)α → β → ε

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)
def function.bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} :
(γ → δ)(α → β → γ)α → β → δ

Compose an unary function f with a binary function g.

Equations
• a b = f (g a b)
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_5out_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
@[instance]
def function.has_uncurry_base {α : Type u_1} {β : Type u_2} :
function.has_uncurry (α → β) α β

Equations
@[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} :
(α → α) → 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 : α → α} :
f f = id

theorem function.involutive.left_inverse {α : Sort u} {f : α → α} :

theorem function.involutive.right_inverse {α : Sort u} {f : α → α} :

theorem function.involutive.injective {α : Sort u} {f : α → α} :

theorem function.involutive.surjective {α : Sort u} {f : α → α} :

theorem function.involutive.bijective {α : Sort u} {f : α → α} :

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.

def function.injective2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} :
(α → β → γ) → 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₂
theorem function.injective2.left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (hf : function.injective2 f) ⦃a₁ a₂ : α⦄ ⦃b₁ b₂ : β⦄ :
f a₁ b₁ = f a₂ b₂a₁ = a₂

theorem function.injective2.right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (hf : function.injective2 f) ⦃a₁ a₂ : α⦄ ⦃b₁ b₂ : β⦄ :
f a₁ b₁ = f a₂ b₂b₁ = b₂

theorem function.injective2.eq_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (hf : function.injective2 f) ⦃a₁ a₂ : α⦄ ⦃b₁ b₂ : β⦄ :
f a₁ b₁ = f a₂ b₂ a₁ = a₂ b₁ = b₂

def function.sometimes {α : Sort u_1} {β : Sort u_2} [nonempty β] :
(α → β) → β

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) :
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