# mathlib3documentation

logic.function.basic

# Miscellaneous function constructions and lemmas #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[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
@[simp]
theorem function.on_fun_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : β β γ) (g : α β) (a b : α) :
(f on g) a b = f (g a) (g b)
@[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₂ f g₁ = 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
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
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
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 a p 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 a f 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 a g x = f x
@[simp]
theorem function.update_eq_self_iff {α : Sort u} {β : α Sort v} [decidable_eq α] {f : Π (a : α), β a} {a : α} {b : β a} :
b = f b = f a
@[simp]
theorem function.eq_update_self_iff {α : Sort u} {β : α Sort v} [decidable_eq α] {f : Π (a : α), β a} {a : α} {b : β a} :
f = b f a = b
theorem function.ne_update_self_iff {α : Sort u} {β : α Sort v} [decidable_eq α] {f : Π (a : α), β a} {a : α} {b : β a} :
f b f a b
theorem function.update_ne_self_iff {α : Sort u} {β : α Sort v} [decidable_eq α] {f : Π (a : α), β a} {a : α} {b : β a} :
b f b 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_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, more generally when `g.factors_through f`.

Equations
def function.factors_through {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (g : α γ) (f : α β) :
Prop

g factors through f : `f a = f b → g a = g b`

Equations
• = ⦃a b : α⦄, f a = f b g a = g b
theorem function.injective.factors_through {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} (hf : function.injective f) (g : α γ) :
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)
theorem function.factors_through.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} {g : α γ} (hf : f) (e' : β γ) (a : α) :
e' (f a) = g a
@[simp]
theorem function.injective.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.factors_through_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} (g : α γ) [nonempty γ] :
(e : β γ), g = e f
theorem function.factors_through.apply_extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} {δ : Sort u_4} {g : α γ} (hf : f) (F : γ δ) (e' : β γ) (b : β) :
F g e' b) = (F g) (F e') b
theorem function.injective.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')
theorem function.factors_through.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} {g : α γ} (e' : β γ) (hf : f) :
e' f = g
@[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)

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