# Miscellaneous function constructions and lemmas #

@[reducible]
def Function.eval {α : Sort u_1} {β : αSort u_4} (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
Instances For
theorem Function.eval_apply {α : Sort u_1} {β : αSort u_4} (x : α) (f : (x : α) → β x) :
= f x
theorem Function.const_def {α : Sort u_1} {β : Sort u_2} {y : β} :
(fun (x : α) => y) =
theorem Function.const_injective {α : Sort u_1} {β : Sort u_2} [] :
@[simp]
theorem Function.const_inj {α : Sort u_1} {β : Sort u_2} [] {y₁ : β} {y₂ : β} :
= y₁ = y₂
theorem Function.onFun_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : ββγ) (g : αβ) (a : α) (b : α) :
(f on g) a b = f (g a) (g b)
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.ne_iff {α : Sort u_1} {β : αSort u_4} {f₁ : (a : α) → β a} {f₂ : (a : α) → β a} :
f₁ f₂ ∃ (a : α), f₁ a f₂ a
theorem Function.funext_iff_of_subsingleton {α : Sort u_1} {β : Sort u_2} {f : αβ} [] {g : αβ} (x : α) (y : α) :
f x = g y f = g
theorem Function.Bijective.injective {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) :
theorem Function.Bijective.surjective {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) :
theorem Function.Injective.eq_iff {α : Sort u_1} {β : Sort u_2} {f : αβ} (I : ) {a : α} {b : α} :
f a = f b a = b
theorem Function.Injective.beq_eq {α : Type u_4} {β : Type u_5} [BEq α] [] [BEq β] [] {f : αβ} (I : ) {a : α} {b : α} :
(f a == f b) = (a == b)
theorem Function.Injective.eq_iff' {α : Sort u_1} {β : Sort u_2} {f : αβ} (I : ) {a : α} {b : α} {c : β} (h : f b = c) :
f a = c a = b
theorem Function.Injective.ne {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) {a₁ : α} {a₂ : α} :
a₁ a₂f a₁ f a₂
theorem Function.Injective.ne_iff {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) {x : α} {y : α} :
f x f y x y
theorem Function.Injective.ne_iff' {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) {x : α} {y : α} {z : β} (h : f y = z) :
f x z x y
theorem Function.not_injective_iff {α : Sort u_1} {β : Sort u_2} {f : αβ} :
∃ (a : α), ∃ (b : α), f a = f b a b
def Function.Injective.decidableEq {α : Sort u_1} {β : Sort u_2} {f : αβ} [] (I : ) :

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

Equations
Instances For
theorem Function.Injective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (I : Function.Injective (f g)) :
@[simp]
theorem Function.Injective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : ) (g : γα) :
theorem Function.Injective.of_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (I : Function.Injective (f g)) (hg : ) :
theorem Function.Surjective.bijective₂_of_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (hf : ) (hg : ) (I : Function.Injective (f g)) :
@[simp]
theorem Function.Injective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβ) {g : γα} (hg : ) :
theorem Function.Injective.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : βγ} (hg : ) :
Function.Injective fun (x : αβ) => g x

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

theorem Function.injective_of_subsingleton {α : Sort u_1} {β : Sort u_2} [] (f : αβ) :
theorem Function.Injective.dite {α : Sort u_1} {β : Sort u_2} (p : αProp) [] {f : { a : α // p a }β} {f' : { a : α // ¬p a }β} (hf : ) (hf' : ) (im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f x, hx f' x', hx') :
Function.Injective fun (x : α) => if h : p x then f x, h else f' x, h
theorem Function.Surjective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (S : Function.Surjective (f g)) :
@[simp]
theorem Function.Surjective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβ) {g : γα} (hg : ) :
theorem Function.Surjective.of_comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (S : Function.Surjective (f g)) (hf : ) :
theorem Function.Injective.bijective₂_of_surjective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (hf : ) (hg : ) (S : Function.Surjective (f g)) :
@[simp]
theorem Function.Surjective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : ) (g : γα) :
instance Function.decidableEqPFun (p : Prop) [] (α : pType u_4) [(hp : p) → DecidableEq (α hp)] :
DecidableEq ((hp : p) → α hp)
Equations
theorem Function.Surjective.forall {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) {p : βProp} :
(∀ (y : β), p y) ∀ (x : α), p (f x)
theorem Function.Surjective.forall₂ {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) {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 : ) {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 : ) {p : βProp} :
(∃ (y : β), p y) ∃ (x : α), p (f x)
theorem Function.Surjective.exists₂ {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) {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 : ) {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.Injective fun (g : βγ) => g f
theorem Function.Surjective.right_cancellable {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : ) {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 : αβ) :
∀ (b : β), ∃! a : α, f a = b
theorem Function.Bijective.existsUnique {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : ) (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 : ) {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 : ) :
theorem Function.Bijective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : ) (g : γα) :
theorem Function.cantor_surjective {α : Type u_4} (f : αSet α) :

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

theorem Function.cantor_injective {α : Type u_4} (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 (max u v). This theorem demonstrates why Type : Type would be inconsistent in Lean.

def Function.IsPartialInv {α : Type u_4} {β : Sort u_5} (f : αβ) (g : β) :

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
Instances For
theorem Function.isPartialInv_left {α : Type u_4} {β : Sort u_5} {f : αβ} {g : β} (H : ) (x : α) :
g (f x) = some x
theorem Function.injective_of_isPartialInv {α : Type u_4} {β : Sort u_5} {f : αβ} {g : β} (H : ) :
theorem Function.injective_of_isPartialInv_right {α : Type u_4} {β : Sort u_5} {f : αβ} {g : β} (H : ) (x : β) (y : β) (b : α) (h₁ : b g x) (h₂ : b g y) :
x = y
theorem Function.LeftInverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : ) :
f g = id
theorem Function.leftInverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} :
f g = id
theorem Function.RightInverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : ) :
g f = id
theorem Function.rightInverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} :
g f = id
theorem Function.LeftInverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : βα} {h : βγ} {i : γβ} (hf : ) (hh : ) :
theorem Function.RightInverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : βα} {h : βγ} {i : γβ} (hf : ) (hh : ) :
theorem Function.LeftInverse.rightInverse {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : ) :
theorem Function.RightInverse.leftInverse {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : ) :
theorem Function.LeftInverse.surjective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : ) :
theorem Function.RightInverse.injective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : ) :
theorem Function.LeftInverse.rightInverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : ) (hf : ) :
theorem Function.LeftInverse.rightInverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : ) (hg : ) :
theorem Function.RightInverse.leftInverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} :
theorem Function.RightInverse.leftInverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} :
theorem Function.LeftInverse.eq_rightInverse {α : Sort u_1} {β : Sort u_2} {f : αβ} {g₁ : βα} {g₂ : βα} (h₁ : ) (h₂ : ) :
g₁ = g₂
noncomputable def Function.partialInv {α : Type u_4} {β : Sort u_5} (f : αβ) (b : β) :

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

Equations
• = if h : ∃ (a : α), f a = b then else none
Instances For
theorem Function.partialInv_of_injective {α : Type u_4} {β : Sort u_5} {f : αβ} (I : ) :
theorem Function.partialInv_left {α : Type u_4} {β : Sort u_5} {f : αβ} (I : ) (x : α) :
noncomputable def Function.invFun {α : Sort u} {β : Sort u_3} [] (f : αβ) :
βα

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

Equations
• = if h : ∃ (x : α), f x = y then h.choose else
Instances For
theorem Function.invFun_eq {α : Sort u_1} {β : Sort u_2} [] {f : αβ} {b : β} (h : ∃ (a : α), f a = b) :
f () = b
theorem Function.apply_invFun_apply {α : Type u_3} {β : Type u_4} {f : αβ} {a : α} :
f (Function.invFun f (f a)) = f a
theorem Function.invFun_neg {α : Sort u_1} {β : Sort u_2} [] {f : αβ} {b : β} (h : ¬∃ (a : α), f a = b) :
theorem Function.invFun_eq_of_injective_of_rightInverse {α : Sort u_1} {β : Sort u_2} [] {f : αβ} {g : βα} (hf : ) (hg : ) :
theorem Function.rightInverse_invFun {α : Sort u_1} {β : Sort u_2} [] {f : αβ} (hf : ) :
theorem Function.leftInverse_invFun {α : Sort u_1} {β : Sort u_2} [] {f : αβ} (hf : ) :
theorem Function.invFun_surjective {α : Sort u_1} {β : Sort u_2} [] {f : αβ} (hf : ) :
theorem Function.invFun_comp {α : Sort u_1} {β : Sort u_2} [] {f : αβ} (hf : ) :
= id
theorem Function.Injective.hasLeftInverse {α : Sort u_1} {β : Sort u_2} [] {f : αβ} (hf : ) :
theorem Function.injective_iff_hasLeftInverse {α : Sort u_1} {β : Sort u_2} [] {f : αβ} :
noncomputable def Function.surjInv {α : Sort u} {β : Sort v} {f : αβ} (h : ) (b : β) :
α

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

Equations
Instances For
theorem Function.surjInv_eq {α : Sort u} {β : Sort v} {f : αβ} (h : ) (b : β) :
f () = b
theorem Function.rightInverse_surjInv {α : Sort u} {β : Sort v} {f : αβ} (hf : ) :
theorem Function.leftInverse_surjInv {α : Sort u} {β : Sort v} {f : αβ} (hf : ) :
theorem Function.Surjective.hasRightInverse {α : Sort u} {β : Sort v} {f : αβ} (hf : ) :
theorem Function.surjective_iff_hasRightInverse {α : Sort u} {β : Sort v} {f : αβ} :
theorem Function.bijective_iff_has_inverse {α : Sort u} {β : Sort v} {f : αβ} :
∃ (g : βα),
theorem Function.injective_surjInv {α : Sort u} {β : Sort v} {f : αβ} (h : ) :
theorem Function.surjective_to_subsingleton {α : Sort u} {β : Sort v} [na : ] [] (f : αβ) :
theorem Function.Surjective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : βγ} (hg : ) :
Function.Surjective fun (x : αβ) => g x

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

theorem Function.Bijective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : βγ} (hg : ) :
Function.Bijective fun (x : αβ) => g x

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

def Function.update {α : Sort u} {β : αSort v} [] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
β a

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

Equations
Instances For
@[simp]
theorem Function.update_same {α : Sort u} {β : αSort v} [] (a : α) (v : β a) (f : (a : α) → β a) :
Function.update f a v a = v
@[simp]
theorem Function.update_noteq {α : Sort u} {β : αSort v} [] {a : α} {a' : α} (h : a a') (v : β a') (f : (a : α) → β a) :
Function.update f a' v a = f a
theorem Function.update_apply {α : Sort u} [] {β : 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

theorem Function.update_eq_const_of_subsingleton {α : Sort u} {α' : Sort w} [] [] (a : α) (v : α') (f : αα') :
=
theorem Function.surjective_eval {α : Sort u} {β : αSort v} [h : ∀ (a : α), Nonempty (β a)] (a : α) :
theorem Function.update_injective {α : Sort u} {β : αSort v} [] (f : (a : α) → β a) (a' : α) :
theorem Function.forall_update_iff {α : Sort u} {β : αSort v} [] (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} [] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β aProp) :
(∃ (x : α), p x (Function.update f a b x)) p a b ∃ (x : α), x a p x (f x)
theorem Function.update_eq_iff {α : Sort u} {β : αSort v} [] {a : α} {b : β a} {f : (a : α) → β a} {g : (a : α) → β a} :
= g b = g a ∀ (x : α), x af x = g x
theorem Function.eq_update_iff {α : Sort u} {β : αSort v} [] {a : α} {b : β a} {f : (a : α) → β a} {g : (a : α) → β a} :
g = g a = b ∀ (x : α), x ag x = f x
@[simp]
theorem Function.update_eq_self_iff {α : Sort u} {β : αSort v} [] {f : (a : α) → β a} {a : α} {b : β a} :
= f b = f a
@[simp]
theorem Function.eq_update_self_iff {α : Sort u} {β : αSort v} [] {f : (a : α) → β a} {a : α} {b : β a} :
f = f a = b
theorem Function.ne_update_self_iff {α : Sort u} {β : αSort v} [] {f : (a : α) → β a} {a : α} {b : β a} :
f f a b
theorem Function.update_ne_self_iff {α : Sort u} {β : αSort v} [] {f : (a : α) → β a} {a : α} {b : β a} :
f b f a
@[simp]
theorem Function.update_eq_self {α : Sort u} {β : αSort v} [] (a : α) (f : (a : α) → β a) :
Function.update f a (f a) = f
theorem Function.update_comp_eq_of_forall_ne' {α : Sort u} {β : αSort v} [] {α' : 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} [] {α : Sort u_1} {β : Sort u_2} (g : α'β) {f : αα'} {i : α'} (a : β) (h : ∀ (x : α), f x i) :
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} [] [] (g : (a : α) → β a) {f : α'α} (hf : ) (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} [] [] {β : Sort u_1} (g : α'β) {f : αα'} (hf : ) (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} [] {α : ι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} [] {α : ι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.pred_update {α : Sort u} {β : αSort v} [] (P : a : α⦄ → β aProp) (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
P (Function.update f a' v a) a = a' P v a a' P (f a)
theorem Function.comp_update {α : Sort u} [] {α' : Sort u_1} {β : Sort u_2} (f : α'β) (g : αα') (i : α) (v : α') :
f = Function.update (f g) i (f v)
theorem Function.update_comm {α : Sort u_2} [] {β : αSort u_1} {a : α} {b : α} (h : a b) (v : β a) (w : β b) (f : (a : α) → β a) :
@[simp]
theorem Function.update_idem {α : Sort u_2} [] {β : αSort u_1} {a : α} (v : β a) (w : β a) (f : (a : α) → β a) :
def Function.extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβ) (g : αγ) (j : βγ) :
βγ

Extension of a function g : α → γ along a function f : α → β.

For every a : α, f a is sent to g a. f might not be surjective, so we use an auxiliary function j : β → γ by sending b : β not in the range of f to j b. If you do not care about the behavior outside the range, j can be used as a junk value by setting it to be 0 or Classical.arbitrary (assuming γ is nonempty).

This definition is mathematically meaningful only when f a₁ = f a₂ → g a₁ = g a₂ (spelled g.FactorsThrough f). In particular this holds if f is injective.

A typical use case is extending a function from a subtype to the entire type. If you wish to extend g : {b : β // p b} → γ to a function β → γ, you should use Function.extend Subtype.val g j.

Equations
Instances For
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

Equations
• = ∀ ⦃a b : α⦄, f a = f bg a = g b
Instances For
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 = if h : ∃ (a : α), f a = b then g () else e' b
theorem Function.Injective.factorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : ) (g : αγ) :
theorem Function.FactorsThrough.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : αγ} (hf : ) (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 : ) (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_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (g : αγ) [] :
∃ (e : βγ), g = e f
theorem Function.apply_extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {g : αγ} (F : γδ) (f : αβ) (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 : ) (e' : βγ) :
Function.Injective fun (g : αγ) => Function.extend f g e'
theorem Function.FactorsThrough.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : αγ} (e' : βγ) (hf : ) :
Function.extend f g e' f = g
@[simp]
theorem Function.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : ) (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 : ) (g₀ : βγ) :
Function.Surjective fun (g : βγ) => g f
theorem Function.Injective.surjective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} [] (hf : ) :
Function.Surjective fun (g : βγ) => g f
theorem Function.Bijective.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : ) :
Function.Bijective fun (g : βγ) => g f
theorem Function.FactorsThrough.rfl {α : Sort u_1} {β : Sort u_2} {f : αβ} :
theorem Function.FactorsThrough.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : αβ} {g : αγ} (h : ) (g' : γδ) :
theorem Function.FactorsThrough.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : αβ} {g : αγ} (h : ) (g' : δα) :
theorem Function.uncurry_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} (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 : β) :
= 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
def Function.bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : γδ) (g : αβγ) (a : α) (b : β) :
δ

Compose a unary function f with a binary function g.

Equations
Instances For
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 Function.HasUncurry (α : Type u_5) (β : outParam (Type u_6)) (γ : outParam (Type u_7)) :
Type (max (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.

• uncurry : αβγ

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

Uncurrying operator. The most generic use is to recursively uncurry. For instance f : α → β → γ → δ will be turned into ↿f : α × β × γ → δ. One can also add instances for bundled maps.

Equations
Instances For
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} [] :
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.

Equations
• = ∀ (x : α), f (f x) = x
Instances For
@[simp]
theorem Function.Involutive.comp_self {α : Sort u} {f : αα} (h : ) :
f f = id
theorem Function.Involutive.leftInverse {α : Sort u} {f : αα} (h : ) :
theorem Function.Involutive.rightInverse {α : Sort u} {f : αα} (h : ) :
theorem Function.Involutive.injective {α : Sort u} {f : αα} (h : ) :
theorem Function.Involutive.surjective {α : Sort u} {f : αα} (h : ) :
theorem Function.Involutive.bijective {α : Sort u} {f : αα} (h : ) :
theorem Function.Involutive.ite_not {α : Sort u} {f : αα} (h : ) (P : Prop) [] (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 : ) {x : α} {y : α} :
f x = y x = f y

An involution commutes across an equality. Compare to Function.Injective.eq_iff.

@[simp]
theorem Function.symmetric_apply_eq_iff {α : Sort u_1} {f : αα} :
(Symmetric fun (x x_1 : α) => f x = x_1)
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
• = ∀ ⦃a₁ a₂ : α⦄ ⦃b₁ b₂ : β⦄, f a₁ b₁ = f a₂ b₂a₁ = a₂ b₁ = b₂
Instances For
theorem Function.Injective2.left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβγ} (hf : ) (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 : ) (a : α) :

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

theorem Function.Injective2.uncurry {α : Type u_4} {β : Type u_5} {γ : Type u_6} {f : αβγ} (hf : ) :
theorem Function.Injective2.left' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβγ} (hf : ) [] :

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.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 : ) {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} :
f a₁ b₁ = f a₂ b₂ a₁ = a₂ b₁ = b₂
noncomputable def Function.sometimes {α : Sort u_1} {β : Sort u_2} [] (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
Instances For
theorem Function.sometimes_eq {p : Prop} {α : Sort u_1} [] (f : pα) (a : p) :
= f a
theorem Function.sometimes_spec {p : Prop} {α : Sort u_1} [] (P : αProp) (f : pα) (a : p) (h : P (f a)) :
P
theorem forall_existsUnique_iff {α : Sort u_1} {β : Sort u_2} {r : αβProp} :
(∀ (a : α), ∃! b : β, r a b) ∃ (f : αβ), ∀ {a : α} {b : β}, r a b f a = b

A relation r : α → β → Prop is "function-like" (for each a there exists a unique b such that r a b) if and only if it is (f · = ·) for some function f.

theorem forall_existsUnique_iff' {α : Sort u_1} {β : Sort u_2} {r : αβProp} :
(∀ (a : α), ∃! b : β, r a b) ∃ (f : αβ), r = fun (x : α) (x_1 : β) => f x = x_1

A relation r : α → β → Prop is "function-like" (for each a there exists a unique b such that r a b) if and only if it is (f · = ·) for some function f.

theorem Symmetric.forall_existsUnique_iff' {α : Sort u_1} {r : ααProp} (hr : ) :
(∀ (a : α), ∃! b : α, r a b) ∃ (f : αα), r = fun (x x_1 : α) => f x = x_1

A symmetric relation r : α → α → Prop is "function-like" (for each a there exists a unique b such that r a b) if and only if it is (f · = ·) for some involutive function f.

theorem Symmetric.forall_existsUnique_iff {α : Sort u_1} {r : ααProp} (hr : ) :
(∀ (a : α), ∃! b : α, r a b) ∃ (f : αα), ∀ {a b : α}, r a b f a = b

A symmetric relation r : α → α → Prop is "function-like" (for each a there exists a unique b such that r a b) if and only if it is (f · = ·) for some involutive function f.

def Set.piecewise {α : Type u} {β : αSort v} (s : Set α) (f : (i : α) → β i) (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
• s.piecewise f g i = if i s then f i else g i
Instances For

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

theorem eq_rec_on_bijective {α : Sort u_1} {C : αSort u_3} {a : α} {a' : α} (h : a = a') :
Function.Bijective fun (x : C a) => hx
theorem eq_mp_bijective {α : Sort u_3} {β : Sort u_3} (h : α = β) :
theorem eq_mpr_bijective {α : Sort u_3} {β : Sort u_3} (h : α = β) :
theorem cast_bijective {α : Sort u_3} {β : Sort u_3} (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_3} (x : C a) (y : C a) :
hx = hy x = y
@[simp]
theorem cast_inj {α : Type u} {β : Type u} (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 : ) (C : (a : α) → γ (f a)) (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 : ) (C : (a : α) → γ (f a)) (a : α) :
Eq.recOn (C (g (f a))) = C a
theorem Function.LeftInverse.cast_eq {α : Sort u_1} {β : Sort u_2} {γ : βSort v} {f : αβ} {g : βα} (h : ) (C : (a : α) → γ (f a)) (a : α) :
cast (C (g (f a))) = C a
def Set.SeparatesPoints {α : Type u_3} {β : Type u_4} (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
• A.SeparatesPoints = ∀ ⦃x y : α⦄, x y∃ (f : αβ), f A f x f y
Instances For
theorem IsSymmOp.flip_eq {α : Sort u_1} {β : Sort u_2} (op : ααβ) [IsSymmOp α β op] :
flip op = op
theorem InvImage.equivalence {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) (h : ) :
instance instDecidableUncurryOfFstSnd {α : Type u_3} {β : Type u_4} {r : αβProp} {x : α × β} [Decidable (r x.fst x.snd)] :
Equations
• instDecidableUncurryOfFstSnd = inst
instance instDecidableCurryOfMk {α : Type u_3} {β : Type u_4} {r : α × βProp} {a : α} {b : β} [Decidable (r (a, b))] :
Equations
• instDecidableCurryOfMk = inst