mathlib3 documentation

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
@[simp]
theorem function.eval_apply {α : Sort u_1} {β : α Sort u_2} (x : α) (f : Π (x : α), β 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) = function.const α y
@[simp]
theorem function.const_apply {α : Sort u_1} {β : Sort u_2} {y : β} {x : α} :
function.const α y x = y
@[simp]
theorem function.const_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} {c : γ} :
@[simp]
theorem function.comp_const {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : β γ} {b : β} :
@[simp]
theorem function.const_inj {α : Sort u_1} {β : Sort u_2} [nonempty α] {y₁ y₂ : β} :
function.const α y₁ = function.const α 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) [decidable_pred p] {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 : α β) :
function.bijective 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 : β 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
theorem function.is_partial_inv_left {α : Type u_1} {β : Sort u_2} {f : α β} {g : β option α} (H : function.is_partial_inv f g) (x : α) :
g (f x) = option.some x
theorem function.injective_of_partial_inv {α : Type u_1} {β : Sort u_2} {f : α β} {g : β option α} (H : function.is_partial_inv f g) :
theorem function.injective_of_partial_inv_right {α : Type u_1} {β : Sort u_2} {f : α β} {g : β option α} (H : function.is_partial_inv f 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 : function.left_inverse f g) :
f g = id
theorem function.left_inverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} :
theorem function.right_inverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} (h : function.right_inverse f g) :
g f = id
theorem function.right_inverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} :
theorem function.left_inverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} {g : β α} {h : β γ} {i : γ β} (hf : function.left_inverse f g) (hh : function.left_inverse h i) :
theorem function.right_inverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} {g : β α} {h : β γ} {i : γ β} (hf : function.right_inverse f g) (hh : function.right_inverse h i) :
theorem function.left_inverse.right_inverse {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} (h : function.left_inverse g f) :
theorem function.right_inverse.left_inverse {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} (h : function.right_inverse g f) :
theorem function.left_inverse.surjective {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} (h : function.left_inverse f g) :
theorem function.right_inverse.injective {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} (h : function.right_inverse f g) :
theorem function.left_inverse.right_inverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} (h : function.left_inverse f g) (hf : function.injective f) :
theorem function.left_inverse.right_inverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : α β} {g : β α} (h : function.left_inverse f g) (hg : function.surjective g) :
theorem function.left_inverse.eq_right_inverse {α : Sort u_1} {β : Sort u_2} {f : α β} {g₁ g₂ : β α} (h₁ : function.left_inverse g₁ f) (h₂ : function.right_inverse g₂ 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_left {α : Type u_1} {β : Sort u_2} {f : α β} (I : function.injective 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) :
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 : function.right_inverse g 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) :
theorem function.injective.has_left_inverse {α : Sort u_1} {β : Sort u_2} [nonempty α] {f : α β} (hf : function.injective 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 : β) :
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
theorem function.update_apply {α : Sort u} [decidable_eq α] {β : Sort u_1} (f : α β) (a' : α) (b : β) (a : α) :
function.update f 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) :
function.update f 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) :
function.update f 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 (function.update f 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 (function.update f 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} :
function.update f 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 = function.update f a 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} :
function.update f 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 = function.update f a b f a = b
theorem function.ne_update_self_iff {α : Sort u} {β : α Sort v} [decidable_eq α] {f : Π (a : α), β a} {a : α} {b : β a} :
f function.update f a b f a b
theorem function.update_ne_self_iff {α : Sort u} {β : α Sort v} [decidable_eq α] {f : Π (a : α), β a} {a : α} {b : β a} :
function.update f a b f b f a
@[simp]
theorem function.update_eq_self {α : Sort u} {β : α Sort v} [decidable_eq α] (a : α) (f : Π (a : α), β a) :
function.update f 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 : α'), function.update g i 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) :
function.update g 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 : α'), function.update g (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 : β) :
function.update g (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 (function.update g 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 (function.update g i v j) (function.update h 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 function.update g i 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) :
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
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)] :
function.extend f g 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 : function.factors_through g f) (e' : β γ) (a : α) :
function.extend f g 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 : α) :
function.extend f g 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) :
function.extend f g e' b = e' b
theorem function.factors_through_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} (g : α γ) [nonempty γ] :
function.factors_through g f (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 : function.factors_through g f) (F : γ δ) (e' : β γ) (b : β) :
F (function.extend f g e' b) = function.extend f (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 (function.extend f g e' b) = function.extend f (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 : α γ), function.extend f g e')
theorem function.factors_through.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} {g : α γ} (e' : β γ) (hf : function.factors_through g f) :
function.extend f g e' f = g
@[simp]
theorem function.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α β} (hf : function.injective f) (g : α γ) (e' : β γ) :
function.extend f g 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 : α β γ) :
function.uncurry 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 : β) :
function.uncurry f (x, y) = f x y
@[simp]
theorem function.curry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α × β γ) (x : α) (y : β) :
function.curry f x 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
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
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 β γ δ] :
function.has_uncurry β) × γ) δ
Equations
def function.involutive {α : Sort u_1} (f : α α) :
Prop

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

Equations
@[simp]
theorem function.involutive.comp_self {α : Sort u} {f : α α} (h : function.involutive f) :
f f = id
@[protected]
@[protected]
@[protected]
@[protected]
@[protected]
@[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
@[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) :
theorem function.sometimes_spec {p : Prop} {α : Sort u_1} [nonempty α] (P : α Prop) (f : p α) (a : p) (h : P (f a)) :
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 : function.left_inverse g 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 : function.left_inverse g 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 : function.left_inverse g 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 : α α β) [is_symm_op α β op] :
flip op = op
theorem inv_image.equivalence {α : Sort u} {β : Sort v} (r : β β Prop) (f : α β) (h : equivalence r) :