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

Function.eval x f = f x

source

ink

theorem Function.eval_apply {α : Sort u_2} {β : α → Sort u_1} (x : α) (f : (x : α) → β x) :

Function.eval x f = f x

source

ink

theorem Function.const_def {α : Sort u_1} {β : Sort u_2} {y : β} :

(fun x => y) = Function.const α y

source

ink

@[simp]

theorem Function.const_comp {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} {f : α → β} {c : γ} :

Function.const β c ∘ f = Function.const α c

source

ink

@[simp]

theorem Function.comp_const {α : Sort u_1} {β : Sort u_3} {γ : Sort u_2} {f : β → γ} {b : β} :

f ∘ Function.const α b = Function.const α (f b)

source

ink

theorem Function.const_injective {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] :

Function.Injective (Function.const α)

source

ink

@[simp]

theorem Function.const_inj {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {y₁ : β} {y₂ : β} :

Function.const α y₁ = Function.const α y₂ ↔ y₁ = y₂

source

ink

theorem Function.id_def {α : Sort u_1} :

id = fun x => x

source

ink

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'

source

ink

theorem Function.funext_iff {α : Sort u_2} {β : α → Sort u_1} {f₁ : (x : α) → β x} {f₂ : (x : α) → β x} :

f₁ = f₂ ↔ ∀ (a : α), f₁ a = f₂ a

source

ink

theorem Function.ne_iff {α : Sort u_2} {β : α → Sort u_1} {f₁ : (a : α) → β a} {f₂ : (a : α) → β a} :

f₁ ≠ f₂ ↔ ∃ a, f₁ a ≠ f₂ a

source

ink

theorem Function.Bijective.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) :

Function.Injective f

source

ink

theorem Function.Bijective.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) :

Function.Surjective f

source

ink

theorem Function.Injective.eq_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : Function.Injective f) {a : α} {b : α} :

f a = f b ↔ a = b

source

ink

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)

source

ink

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

source

ink

theorem Function.Injective.ne {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Injective f) {a₁ : α} {a₂ : α} :

a₁ ≠ a₂ → f a₁ ≠ f a₂

source

ink

theorem Function.Injective.ne_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Injective f) {x : α} {y : α} :

f x ≠ f y ↔ x ≠ y

source

ink

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

source

ink

def Function.Injective.decidableEq {α : Sort u_1} {β : Sort u_2} {f : α → β} [inst : DecidableEq β] (I : Function.Injective f) :

DecidableEq α

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

Equations

Function.Injective.decidableEq I x x = decidable_of_iff (f x = f x) (_ : f x = f x ↔ x = x)

source

ink

theorem Function.Injective.of_comp {α : Sort u_3} {β : Sort u_2} {γ : Sort u_1} {f : α → β} {g : γ → α} (I : Function.Injective (f ∘ g)) :

Function.Injective g

source

ink

theorem Function.Injective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (g : γ → α) :

Function.Injective (f ∘ g) ↔ Function.Injective g

source

ink

theorem Function.Injective.of_comp_iff' {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} (f : α → β) {g : γ → α} (hg : Function.Bijective g) :

Function.Injective (f ∘ g) ↔ Function.Injective f

source

ink

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.

source

ink

theorem Function.injective_of_subsingleton {α : Sort u_1} {β : Sort u_2} [inst : Subsingleton α] (f : α → β) :

Function.Injective f

source

ink

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 }

source

ink

theorem Function.Surjective.of_comp {α : Sort u_3} {β : Sort u_2} {γ : Sort u_1} {f : α → β} {g : γ → α} (S : Function.Surjective (f ∘ g)) :

Function.Surjective f

source

ink

theorem Function.Surjective.of_comp_iff {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} (f : α → β) {g : γ → α} (hg : Function.Surjective g) :

Function.Surjective (f ∘ g) ↔ Function.Surjective f

source

ink

theorem Function.Surjective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Bijective f) (g : γ → α) :

Function.Surjective (f ∘ g) ↔ Function.Surjective g

source

ink

instance Function.decidableEqPfun (p : Prop) [inst : Decidable p] (α : p → Type u_1) [inst : (hp : p) → DecidableEq (α hp)] :

DecidableEq ((hp : p) → α hp)

Equations

Function.decidableEqPfun p α x x = match x, x with | f, g => decidable_of_iff (∀ (hp : p), f hp = g hp) (_ : (∀ (a : p), f a = g a) ↔ (fun hp => f hp) = fun hp => g hp)

source

ink

theorem Function.Surjective.forall {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Surjective f) {p : β → Prop} :

((y : β) → p y) ↔ (x : α) → p (f x)

source

ink

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

source

ink

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

source

ink

theorem Function.Surjective.exists {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Surjective f) {p : β → Prop} :

(∃ y, p y) ↔ ∃ x, p (f x)

source

ink

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

source

ink

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

source

ink

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

source

ink

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₂

source

ink

theorem Function.surjective_of_right_cancellable_Prop {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : ∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂) :

Function.Surjective f

source

ink

theorem Function.bijective_iff_existsUnique {α : Sort u_1} {β : Sort u_2} (f : α → β) :

Function.Bijective f ↔ ∀ (b : β), ∃! a, f a = b

source

ink

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.

source

ink

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)

source

ink

theorem Function.Bijective.of_comp_iff {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} (f : α → β) {g : γ → α} (hg : Function.Bijective g) :

Function.Bijective (f ∘ g) ↔ Function.Bijective f

source

ink

theorem Function.Bijective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Bijective f) (g : γ → α) :

Function.Bijective (f ∘ g) ↔ Function.Bijective g

source

ink

theorem Function.cantor_surjective {α : Type u_1} (f : α → Set α) :

¬Function.Surjective f

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

source

ink

theorem Function.cantor_injective {α : Type u_1} (f : Set α → α) :

¬Function.Injective f

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

source

ink

theorem Function.not_surjective_Type {α : Type u} (f : α → Type (maxuv)) :

¬Function.Surjective f

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

source

ink

def Function.IsPartialInv {α : 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

Function.IsPartialInv f g = ∀ (x : α) (y : β), g y = some x ↔ f x = y

source

ink

theorem Function.isPartialInv_left {α : Type u_1} {β : Sort u_2} {f : α → β} {g : β → Option α} (H : Function.IsPartialInv f g) (x : α) :

g (f x) = some x

source

ink

theorem Function.injective_of_isPartialInv {α : Type u_1} {β : Sort u_2} {f : α → β} {g : β → Option α} (H : Function.IsPartialInv f g) :

Function.Injective f

source

ink

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

source

ink

theorem Function.LeftInverse.comp_eq_id {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) :

f ∘ g = id

source

ink

theorem Function.leftInverse_iff_comp {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} :

Function.LeftInverse f g ↔ f ∘ g = id

source

ink

theorem Function.RightInverse.comp_eq_id {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} (h : Function.RightInverse f g) :

g ∘ f = id

source

ink

theorem Function.rightInverse_iff_comp {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} :

Function.RightInverse f g ↔ g ∘ f = id

source

ink

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

Function.LeftInverse (h ∘ f) (g ∘ i)

source

ink

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

Function.RightInverse (h ∘ f) (g ∘ i)

source

ink

theorem Function.LeftInverse.rightInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.LeftInverse g f) :

Function.RightInverse f g

source

ink

theorem Function.RightInverse.leftInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.RightInverse g f) :

Function.LeftInverse f g

source

ink

theorem Function.LeftInverse.surjective {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) :

Function.Surjective f

source

ink

theorem Function.RightInverse.injective {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} (h : Function.RightInverse f g) :

Function.Injective f

source

ink

theorem Function.LeftInverse.rightInverse_of_injective {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) (hf : Function.Injective f) :

Function.RightInverse f g

source

ink

theorem Function.LeftInverse.rightInverse_of_surjective {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) (hg : Function.Surjective g) :

Function.RightInverse f g

source

ink

theorem Function.RightInverse.leftInverse_of_surjective {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} :

Function.RightInverse f g → Function.Surjective f → Function.LeftInverse f g

source

ink

theorem Function.RightInverse.leftInverse_of_injective {α : Sort u_2} {β : Sort u_1} {f : α → β} {g : β → α} :

Function.RightInverse f g → Function.Injective g → Function.LeftInverse f g

source

ink

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₂

source

ink

noncomputable def Function.partialInv {α : Type u_1} {β : Sort u_2} (f : α → β) (b : β) :

Option α

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

Equations

Function.partialInv f b = if h : ∃ a, f a = b then some (Classical.choose h) else none

source

ink

theorem Function.partialInv_of_injective {α : Type u_1} {β : Sort u_2} {f : α → β} (I : Function.Injective f) :

Function.IsPartialInv f (Function.partialInv f)

source

ink

theorem Function.partialInv_left {α : Type u_1} {β : Sort u_2} {f : α → β} (I : Function.Injective f) (x : α) :

Function.partialInv f (f x) = some x

source

ink

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

Function.invFun f y = if h : ∃ x, f x = y then Exists.choose h else Classical.arbitrary α

source

ink

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

source

ink

theorem Function.invFun_neg {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} {b : β} (h : ¬∃ a, f a = b) :

Function.invFun f b = Classical.choice inst

source

ink

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

Function.invFun f = g

source

ink

theorem Function.rightInverse_invFun {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} (hf : Function.Surjective f) :

Function.RightInverse (Function.invFun f) f

source

ink

theorem Function.leftInverse_invFun {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} (hf : Function.Injective f) :

Function.LeftInverse (Function.invFun f) f

source

ink

theorem Function.invFun_surjective {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} (hf : Function.Injective f) :

Function.Surjective (Function.invFun f)

source

ink

theorem Function.invFun_comp {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} (hf : Function.Injective f) :

Function.invFun f ∘ f = id

source

ink

theorem Function.Injective.hasLeftInverse {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} (hf : Function.Injective f) :

Function.HasLeftInverse f

source

ink

theorem Function.injective_iff_hasLeftInverse {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} :

Function.Injective f ↔ Function.HasLeftInverse f

source

ink

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

Function.surjInv h b = Classical.choose (h b)

source

ink

theorem Function.surjInv_eq {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β) :

f (Function.surjInv h b) = b

source

ink

theorem Function.rightInverse_surjInv {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Surjective f) :

Function.RightInverse (Function.surjInv hf) f

source

ink

theorem Function.leftInverse_surjInv {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Bijective f) :

Function.LeftInverse (Function.surjInv (_ : Function.Surjective f)) f

source

ink

theorem Function.Surjective.hasRightInverse {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Surjective f) :

Function.HasRightInverse f

source

ink

theorem Function.surjective_iff_hasRightInverse {α : Sort u} {β : Sort v} {f : α → β} :

Function.Surjective f ↔ Function.HasRightInverse f

source

ink

theorem Function.bijective_iff_has_inverse {α : Sort u} {β : Sort v} {f : α → β} :

Function.Bijective f ↔ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f

source

ink

theorem Function.injective_surjInv {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) :

Function.Injective (Function.surjInv h)

source

ink

theorem Function.surjective_to_subsingleton {α : Sort u} {β : Sort v} [na : Nonempty α] [inst : Subsingleton β] (f : α → β) :

Function.Surjective f

source

ink

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.

source

ink

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.

source

ink

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

Function.update f a' v a = if h : a = a' then (_ : a' = a) ▸ v else f a

source

ink

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

source

ink

@[simp]

theorem Function.update_same {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (a : α) (v : β a) (f : (a : α) → β a) :

Function.update f a v a = v

source

ink

theorem Function.surjective_eval {α : Sort u} {β : α → Sort v} [h : ∀ (a : α), Nonempty (β a)] (a : α) :

Function.Surjective (Function.eval a)

source

ink

theorem Function.update_injective {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (f : (a : α) → β a) (a' : α) :

Function.Injective (Function.update f a')

source

ink

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

source

ink

theorem Function.forall_update_iff {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (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))

source

ink

theorem Function.exists_update_iff {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β a → Prop) :

(∃ x, p x (Function.update f a b x)) ↔ p a b ∨ ∃ x x_1, p x (f x)

source

ink

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 ≠ a → f x = g x

source

ink

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 ≠ a → g x = f x

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

@[simp]

theorem Function.update_eq_self {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (a : α) (f : (a : α) → β a) :

Function.update f a (f a) = f

source

ink

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)

source

ink

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'

source

ink

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

source

ink

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'

source

ink

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

source

ink

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

source

ink

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)

source

ink

theorem Function.update_comm {α : Sort u_1} [inst : DecidableEq α] {β : α → Sort u_2} {a : α} {b : α} (h : a ≠ b) (v : β a) (w : β b) (f : (a : α) → β a) :

Function.update (Function.update f a v) b w = Function.update (Function.update f b w) a v

source

ink

@[simp]

theorem Function.update_idem {α : Sort u_1} [inst : DecidableEq α] {β : α → Sort u_2} {a : α} (v : β a) (w : β a) (f : (a : α) → β a) :

Function.update (Function.update f a v) a w = Function.update f a w

source

ink

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

Function.extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b

source

ink

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

Prop

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

Equations

Function.FactorsThrough g f = ∀ ⦃a b : α⦄, f a = f b → g a = g b

source

ink

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

source

ink

theorem Function.Injective.FactorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (g : α → γ) :

Function.FactorsThrough g f

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

theorem Function.extend_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (e' : β → γ) :

Function.Injective fun g => Function.extend f g e'

source

ink

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

source

ink

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

source

ink

theorem Function.Injective.surjective_comp_right' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (g₀ : β → γ) :

Function.Surjective fun g => g ∘ f

source

ink

theorem Function.Injective.surjective_comp_right {α : Sort u_2} {β : Sort u_3} {γ : Sort u_1} {f : α → β} [inst : Nonempty γ] (hf : Function.Injective f) :

Function.Surjective fun g => g ∘ f

source

ink

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

source

ink

theorem Function.uncurry_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) :

Function.uncurry f = fun p => f p.fst p.snd

source

ink

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

source

ink

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

source

ink

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

Function.bicompl f g h a b = f (g a) (h b)

source

ink

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

Function.bicompr f g a b = f (g a b)

source

ink

theorem Function.uncurry_bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_4} {δ : Type u_3} (f : α → β → γ) (g : γ → δ) :

Function.uncurry (Function.bicompr g f) = g ∘ Function.uncurry f

source

ink

theorem Function.uncurry_bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_4} {δ : Type u_5} {ε : Type u_3} (f : γ → δ → ε) (g : α → γ) (h : β → δ) :

Function.uncurry (Function.bicompl f g h) = Function.uncurry f ∘ Prod.map g h

source

ink

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

source

ink

def Function.«term↿_» :

Lean.ParserDescr

Equations

Function.«term↿_» = Lean.ParserDescr.node `Function.term↿_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↿") (Lean.ParserDescr.cat `term 1023))

source

ink

instance Function.hasUncurryBase {α : Type u_1} {β : Type u_2} :

Function.HasUncurry (α → β) α β

Equations

Function.hasUncurryBase = { uncurry := id }

source

ink

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 }

source

ink

def Function.Involutive {α : Sort u_1} (f : α → α) :

Prop

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

Equations

Function.Involutive f = ∀ (x : α), f (f x) = x

source

ink

theorem Function.involutive_iff_iter_2_eq_id {α : Sort u_1} {f : α → α} :

Function.Involutive f ↔ f^[2] = id

source

ink

theorem Bool.involutive_not :

Function.Involutive not

source

ink

@[simp]

theorem Function.Involutive.comp_self {α : Sort u} {f : α → α} (h : Function.Involutive f) :

f ∘ f = id

source

ink

theorem Function.Involutive.leftInverse {α : Sort u} {f : α → α} (h : Function.Involutive f) :

Function.LeftInverse f f

source

ink

theorem Function.Involutive.rightInverse {α : Sort u} {f : α → α} (h : Function.Involutive f) :

Function.RightInverse f f

source

ink

theorem Function.Involutive.injective {α : Sort u} {f : α → α} (h : Function.Involutive f) :

Function.Injective f

source

ink

theorem Function.Involutive.surjective {α : Sort u} {f : α → α} (h : Function.Involutive f) :

Function.Surjective f

source

ink

theorem Function.Involutive.bijective {α : Sort u} {f : α → α} (h : Function.Involutive f) :

Function.Bijective f

source

ink

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.

source

ink

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.

source

ink

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

Function.Injective2 f = ∀ ⦃a₁ a₂ : α⦄ ⦃b₁ b₂ : β⦄, f a₁ b₁ = f a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂

source

ink

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.

source

ink

theorem Function.Injective2.right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) (a : α) :

Function.Injective (f a)

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

source

ink

theorem Function.Injective2.uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} (hf : Function.Injective2 f) :

Function.Injective (Function.uncurry f)

source

ink

theorem Function.Injective2.left' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) [inst : Nonempty β] :

Function.Injective f

As a map from the left argument to a unary function, f is injective.

source

ink

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.

source

ink

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₂

source

ink

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

Function.sometimes f = if h : Nonempty α then f (Classical.choice h) else Classical.choice inst

source

ink

theorem Function.sometimes_eq {p : Prop} {α : Sort u_1} [inst : Nonempty α] (f : p → α) (a : p) :

Function.sometimes f = f a

source

ink

theorem Function.sometimes_spec {p : Prop} {α : Sort u_1} [inst : Nonempty α] (P : α → Prop) (f : p → α) (a : p) (h : P (f a)) :

P (Function.sometimes f)

source

ink

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

Set.piecewise s f g i = if i ∈ s then f i else g i

Bijectivity of `eq.rec`, `eq.mp`, `eq.mpr`, and `cast` #

source

ink

theorem eq_rec_on_bijective {α : Sort u_1} {C : α → Sort u_2} {a : α} {a' : α} (h : a = a') :

Function.Bijective fun x => h ▸ x

source

ink

theorem eq_mp_bijective {α : Sort u_1} {β : Sort u_1} (h : α = β) :

Function.Bijective (Eq.mp h)

source

ink

theorem eq_mpr_bijective {α : Sort u_1} {β : Sort u_1} (h : α = β) :

Function.Bijective (Eq.mpr h)

source

ink

theorem cast_bijective {α : Sort u_1} {β : Sort u_1} (h : α = β) :

Function.Bijective (cast h)

Note these lemmas apply to Type _ not Sort*, as the latter interferes with simp, and is trivial anyway.

source

ink

@[simp]

theorem eq_rec_inj {α : Sort u_1} {a : α} {a' : α} (h : a = a') {C : α → Type u_2} (x : C a) (y : C a) :

h ▸ x = h ▸ y ↔ x = y

source

ink

@[simp]

theorem cast_inj {α : Type u_1} {β : Type u_1} (h : α = β) {x : α} {y : α} :

cast h x = cast h y ↔ x = y

source

ink

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

source

ink

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

source

ink

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

source

ink

def Set.SeparatesPoints {α : 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

Set.SeparatesPoints A = ∀ ⦃x y : α⦄, x ≠ y → ∃ f, f ∈ A ∧ f x ≠ f y

source

ink

theorem IsSymmOp.flip_eq {α : Type u_1} {β : Type u_2} (op : α → α → β) [inst : IsSymmOp α β op] :

flip op = op

source

ink

theorem InvImage.equivalence {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (h : Equivalence r) :

Equivalence (InvImage r f)

Miscellaneous function constructions and lemmas #

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

Bijectivity of `eq.rec`, `eq.mp`, `eq.mpr`, and `cast` #