Documentation

Mathlib.Logic.Function.Basic

Miscellaneous function constructions and lemmas #

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∀ x, β x) → β x→ β x.

Equations
theorem Function.eval_apply {α : Sort u_2} {β : αSort u_1} (x : α) (f : (x : α) → β x) :
theorem Function.const_def {α : Sort u_1} {β : Sort u_2} {y : β} :
(fun x => y) = Function.const α y
@[simp]
theorem Function.const_comp {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} {f : αβ} {c : γ} :
@[simp]
theorem Function.comp_const {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} {f : βγ} {b : β} :
@[simp]
theorem Function.const_inj {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {y₁ : β} {y₂ : β} :
Function.const α y₁ = Function.const α y₂ y₁ = y₂
theorem Function.id_def {α : Sort u_1} :
id = fun x => x
theorem Function.hfunext {α : Sort u} {α' : Sort u} {β : αSort v} {β' : α'Sort v} {f : (a : α) → β a} {f' : (a : α') → β' a} (hα : α = α') (h : ∀ (a : α) (a' : α'), HEq a a'HEq (f a) (f' a')) :
HEq f f'
theorem Function.funext_iff {α : Sort u_2} {β : αSort u_1} {f₁ : (x : α) → β x} {f₂ : (x : α) → β x} :
f₁ = f₂ ∀ (a : α), f₁ a = f₂ a
theorem Function.ne_iff {α : Sort u_2} {β : αSort u_1} {f₁ : (a : α) → β a} {f₂ : (a : α) → β a} :
f₁ f₂ a, f₁ a f₂ a
theorem Function.Bijective.injective {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : Function.Bijective f) :
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.beq_eq {α : Type u_1} {β : Type u_2} {f : αβ} [inst : BEq α] [inst : LawfulBEq α] [inst : BEq β] [inst : LawfulBEq β] (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
def Function.Injective.decidableEq {α : Sort u_1} {β : Sort u_2} {f : αβ} [inst : DecidableEq β] (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_3} {β : Sort u_2} {γ : Sort u_1} {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_2} {β : Sort u_3} {γ : Sort u_1} (f : αβ) {g : γα} (hg : Function.Bijective g) :
theorem Function.Injective.comp_left {α : Sort u_3} {β : Sort u_1} {γ : Sort u_2} {g : βγ} (hg : Function.Injective g) :
Function.Injective ((fun x x_1 => x x_1) g)

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

theorem Function.injective_of_subsingleton {α : Sort u_1} {β : Sort u_2} [inst : Subsingleton α] (f : αβ) :
theorem Function.Injective.dite {α : Sort u_1} {β : Sort u_2} (p : αProp) [inst : DecidablePred 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 { val := x, property := hx } f' { val := x', property := hx' }) :
Function.Injective fun x => if h : p x then f { val := x, property := h } else f' { val := x, property := h }
theorem Function.Surjective.of_comp {α : Sort u_3} {β : Sort u_2} {γ : Sort u_1} {f : αβ} {g : γα} (S : Function.Surjective (f g)) :
theorem Function.Surjective.of_comp_iff {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} (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 : γα) :
instance Function.decidableEqPfun (p : Prop) [inst : Decidable p] (α : pType u_1) [inst : (hp : p) → DecidableEq (α hp)] :
DecidableEq ((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.Surjective.injective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Surjective f) :
Function.Injective fun g => g f
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_existsUnique {α : Sort u_1} {β : Sort u_2} (f : αβ) :
Function.Bijective f ∀ (b : β), ∃! a, f a = b
theorem Function.Bijective.existsUnique {α : 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_existsUnique.

theorem Function.Bijective.existsUnique_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_2} {β : Sort u_3} {γ : Sort u_1} (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 (maxuv)) :

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

def Function.IsPartialInv {α : Type u_1} {β : Sort u_2} (f : αβ) (g : βOption α) :

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.isPartialInv_left {α : Type u_1} {β : Sort u_2} {f : αβ} {g : βOption α} (H : Function.IsPartialInv f g) (x : α) :
g (f x) = some x
theorem Function.injective_of_isPartialInv {α : Type u_1} {β : Sort u_2} {f : αβ} {g : βOption α} (H : Function.IsPartialInv f g) :
theorem Function.injective_of_isPartialInv_right {α : Type u_1} {β : Sort u_2} {f : αβ} {g : βOption α} (H : Function.IsPartialInv f g) (x : β) (y : β) (b : α) (h₁ : b g x) (h₂ : b g y) :
x = y
theorem Function.LeftInverse.comp_eq_id {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} (h : Function.LeftInverse f g) :
f g = id
theorem Function.leftInverse_iff_comp {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} :
theorem Function.RightInverse.comp_eq_id {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} (h : Function.RightInverse f g) :
g f = id
theorem Function.rightInverse_iff_comp {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} :
theorem Function.LeftInverse.comp {α : Sort u_2} {β : Sort u_1} {γ : Sort u_3} {f : αβ} {g : βα} {h : βγ} {i : γβ} (hf : Function.LeftInverse f g) (hh : Function.LeftInverse h i) :
theorem Function.RightInverse.comp {α : Sort u_2} {β : Sort u_1} {γ : Sort u_3} {f : αβ} {g : βα} {h : βγ} {i : γβ} (hf : Function.RightInverse f g) (hh : Function.RightInverse h i) :
theorem Function.LeftInverse.rightInverse {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : Function.LeftInverse g f) :
theorem Function.RightInverse.leftInverse {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : Function.RightInverse g f) :
theorem Function.LeftInverse.surjective {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} (h : Function.LeftInverse f g) :
theorem Function.RightInverse.injective {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} (h : Function.RightInverse f g) :
theorem Function.LeftInverse.rightInverse_of_injective {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} (h : Function.LeftInverse f g) (hf : Function.Injective f) :
theorem Function.LeftInverse.rightInverse_of_surjective {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} (h : Function.LeftInverse f g) (hg : Function.Surjective g) :
theorem Function.RightInverse.leftInverse_of_surjective {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} :
theorem Function.RightInverse.leftInverse_of_injective {α : Sort u_2} {β : Sort u_1} {f : αβ} {g : βα} :
theorem Function.LeftInverse.eq_rightInverse {α : Sort u_1} {β : Sort u_2} {f : αβ} {g₁ : βα} {g₂ : βα} (h₁ : Function.LeftInverse g₁ f) (h₂ : Function.RightInverse g₂ f) :
g₁ = g₂
noncomputable def Function.partialInv {α : 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.partialInv_left {α : Type u_1} {β : Sort u_2} {f : αβ} (I : Function.Injective f) (x : α) :
noncomputable def Function.invFun {α : Sort u} {β : Sort u_1} [inst : 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.invFun_eq {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : αβ} {b : β} (h : a, f a = b) :
f (Function.invFun f b) = b
theorem Function.invFun_neg {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : αβ} {b : β} (h : ¬a, f a = b) :
theorem Function.invFun_eq_of_injective_of_rightInverse {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : αβ} {g : βα} (hf : Function.Injective f) (hg : Function.RightInverse g f) :
theorem Function.rightInverse_invFun {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : αβ} (hf : Function.Surjective f) :
theorem Function.leftInverse_invFun {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : αβ} (hf : Function.Injective f) :
theorem Function.invFun_surjective {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : αβ} (hf : Function.Injective f) :
theorem Function.invFun_comp {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : αβ} (hf : Function.Injective f) :
theorem Function.Injective.hasLeftInverse {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : αβ} (hf : Function.Injective f) :
noncomputable def Function.surjInv {α : Sort u} {β : Sort v} {f : αβ} (h : Function.Surjective f) (b : β) :
α

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

Equations
theorem Function.surjInv_eq {α : Sort u} {β : Sort v} {f : αβ} (h : Function.Surjective f) (b : β) :
theorem Function.surjective_to_subsingleton {α : Sort u} {β : Sort v} [na : Nonempty α] [inst : Subsingleton β] (f : αβ) :
theorem Function.Surjective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : βγ} (hg : Function.Surjective g) :
Function.Surjective ((fun x x_1 => x x_1) 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) :
Function.Bijective ((fun x x_1 => x x_1) g)

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

def Function.update {α : Sort u} {β : αSort v} [inst : DecidableEq α] (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} [inst : DecidableEq α] {β : Sort u_1} (f : αβ) (a' : α) (b : β) (a : α) :
Function.update f a' b a = if a = a' then b else f a

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

@[simp]
theorem Function.update_same {α : Sort u} {β : αSort v} [inst : DecidableEq α] (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} [inst : DecidableEq α] (f : (a : α) → β a) (a' : α) :
@[simp]
theorem Function.update_noteq {α : Sort u} {β : αSort v} [inst : DecidableEq α] {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} [inst : DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β aProp) :
((x : α) → p x (Function.update f a b x)) p a b ((x : α) → x ap x (f x))
theorem Function.exists_update_iff {α : Sort u} {β : αSort v} [inst : DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β aProp) :
(x, p x (Function.update f a b x)) p a b x x_1, p x (f x)
theorem Function.update_eq_iff {α : Sort u} {β : αSort v} [inst : DecidableEq α] {a : α} {b : β a} {f : (a : α) → β a} {g : (a : α) → β a} :
Function.update f a b = g b = g a ∀ (x : α), x af x = g x
theorem Function.eq_update_iff {α : Sort u} {β : αSort v} [inst : DecidableEq α] {a : α} {b : β a} {f : (a : α) → β a} {g : (a : α) → β a} :
g = Function.update f a b g a = b ∀ (x : α), x ag x = f x
@[simp]
theorem Function.update_eq_self_iff {α : Sort u} {β : αSort v} [inst : DecidableEq α] {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} [inst : DecidableEq α] {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} [inst : DecidableEq α] {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} [inst : DecidableEq α] {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} [inst : DecidableEq α] (a : α) (f : (a : α) → β a) :
Function.update f a (f a) = f
theorem Function.update_comp_eq_of_forall_ne' {α : Sort u} {β : αSort v} [inst : DecidableEq α] {α' : Sort u_1} (g : (a : α) → β a) {f : α'α} {i : α} (a : β i) (h : ∀ (x : α'), f x i) :
(fun j => Function.update g i a (f j)) = fun j => g (f j)
theorem Function.update_comp_eq_of_forall_ne {α' : Sort w} [inst : DecidableEq α'] {α : 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} [inst : DecidableEq α] [inst : DecidableEq α'] (g : (a : α) → β a) {f : α'α} (hf : Function.Injective f) (i : α') (a : β (f i)) :
(fun j => Function.update g (f i) a (f j)) = Function.update (fun i => g (f i)) i a
theorem Function.update_comp_eq_of_injective {α : Sort u} {α' : Sort w} [inst : DecidableEq α] [inst : DecidableEq α'] {β : 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} [inst : DecidableEq ι] {α : ι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 (fun k => f k (g k)) i (f i v) j
theorem Function.apply_update₂ {ι : Sort u_1} [inst : DecidableEq ι] {α : ι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 (fun k => f k (g k) (h k)) i (f i v w) j
theorem Function.comp_update {α : Sort u} [inst : DecidableEq α] {α' : 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} [inst : DecidableEq α] {β : αSort u_2} {a : α} {b : α} (h : a b) (v : β a) (w : β b) (f : (a : α) → β a) :
@[simp]
theorem Function.update_idem {α : Sort u_1} [inst : DecidableEq α] {β : αSort u_2} {a : α} (v : β a) (w : β a) (f : (a : α) → β a) :
def Function.extend {α : Sort u} {β : Sort u_1} {γ : Sort u_2} (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, or more generally when g.factors_through f

Equations
def Function.FactorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (g : αγ) (f : αβ) :

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

Equations
theorem Function.extend_def {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβ) (g : αγ) (e' : βγ) (b : β) [inst : Decidable (a, f a = b)] :
Function.extend f g e' b = if h : a, f a = b then g (Classical.choose h) else e' b
theorem Function.Injective.FactorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Injective f) (g : αγ) :
theorem Function.FactorsThrough.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : αγ} (hf : Function.FactorsThrough 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.factorsThrough_iff {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} {f : αβ} (g : αγ) [inst : Nonempty γ] :
Function.FactorsThrough g f e, g = e f
theorem Function.FactorsThrough.apply_extend {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} {f : αβ} {δ : Sort u_1} {g : αγ} (hf : Function.FactorsThrough 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_2} {β : Sort u_3} {γ : Sort u_4} {f : αβ} {δ : Sort u_1} (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' : βγ) :
theorem Function.FactorsThrough.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : αγ} (e' : βγ) (hf : Function.FactorsThrough 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₀ : βγ) :
theorem Function.Injective.surjective_comp_right {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} {f : αβ} [inst : Nonempty γ] (hf : Function.Injective f) :
theorem Function.Bijective.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Bijective f) :
Function.Bijective fun g => g f
theorem Function.uncurry_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) :
Function.uncurry f = fun 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
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
theorem Function.uncurry_bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_4} {δ : Type u_3} (f : αβγ) (g : γδ) :
theorem Function.uncurry_bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_4} {δ : Type u_5} {ε : Type u_3} (f : γδε) (g : αγ) (h : βδ) :
class Function.HasUncurry (α : Type u_1) (β : outParam (Type u_2)) (γ : outParam (Type u_3)) :
Type (max(maxu_1u_2)u_3)
  • Uncurrying operator. The most generic use is to recursively uncurry. For instance f : α → β → γ → δ→ β → γ → δ→ γ → δ→ δ will be turned into ↿f : α × β × γ → δ↿f : α × β × γ → δ× β × γ → δ× γ → δ→ δ. One can also add instances for bundled maps.

    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 : α × β × γ → δ↿f : α × β × γ → δ× β × γ → δ× γ → δ→ δ. One can also add instances for bundled maps.

Instances
    instance Function.hasUncurryBase {α : Type u_1} {β : Type u_2} :
    Function.HasUncurry (αβ) α β
    Equations
    • Function.hasUncurryBase = { uncurry := id }
    instance Function.hasUncurryInduction {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : Function.HasUncurry β γ δ] :
    Function.HasUncurry (αβ) (α × γ) δ
    Equations
    • Function.hasUncurryInduction = { uncurry := fun f p => ((f p.fst)) p.snd }
    def Function.Involutive {α : Sort u_1} (f : αα) :

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

    Equations
    @[simp]
    theorem Function.Involutive.comp_self {α : Sort u} {f : αα} (h : Function.Involutive f) :
    f f = id
    theorem Function.Involutive.ite_not {α : Sort u} {f : αα} (h : Function.Involutive f) (P : Prop) [inst : Decidable P] (x : α) :
    f (if P then x else f x) = if ¬P then x else f x

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

    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 : αβγ) :

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

    Equations
    theorem Function.Injective2.left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβγ} (hf : Function.Injective2 f) (b : β) :
    Function.Injective fun a => f a b

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

    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.

    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) [inst : 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) [inst : Nonempty α] :
    Function.Injective fun 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} [inst : 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} [inst : Nonempty α] (f : pα) (a : p) :
    theorem Function.sometimes_spec {p : Prop} {α : Sort u_1} [inst : Nonempty α] (P : αProp) (f : pα) (a : p) (h : P (f a)) :
    def Set.piecewise {α : Type u} {β : αSort v} (s : Set α) (f : (i : α) → β i) (g : (i : α) → β i) [inst : (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') :
    Function.Bijective fun x => hx
    theorem eq_mp_bijective {α : Sort u_1} {β : Sort u_1} (h : α = β) :
    theorem eq_mpr_bijective {α : Sort u_1} {β : Sort u_1} (h : α = β) :
    theorem cast_bijective {α : Sort u_1} {β : 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 : C a) (y : C a) :
    hx = hy x = y
    @[simp]
    theorem cast_inj {α : Type u_1} {β : Type u_1} (h : α = β) {x : α} {y : α} :
    cast h x = cast h y x = y
    theorem Function.LeftInverse.eq_rec_eq {α : Sort u_1} {β : Sort u_2} {γ : βSort v} {f : αβ} {g : βα} (h : Function.LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
    (_ : f (g (f a)) = f a)C (g (f a)) = C a
    theorem Function.LeftInverse.eq_rec_on_eq {α : Sort u_1} {β : Sort u_2} {γ : βSort v} {f : αβ} {g : βα} (h : Function.LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
    Eq.recOn (_ : f (g (f a)) = f a) (C (g (f a))) = C a
    theorem Function.LeftInverse.cast_eq {α : Sort u_1} {β : Sort u_2} {γ : βSort v} {f : αβ} {g : βα} (h : Function.LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
    cast (_ : γ (f (g (f a))) = γ (f a)) (C (g (f a))) = C a
    def Set.SeparatesPoints {α : Type u_1} {β : Type u_2} (A : Set (αβ)) :

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

    Equations
    theorem IsSymmOp.flip_eq {α : Type u_1} {β : Type u_2} (op : ααβ) [inst : IsSymmOp α β op] :
    flip op = op
    theorem InvImage.equivalence {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) (h : Equivalence r) :