General operations on functions

theorem Function.flip_def {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {f : α → β → φ} : flip f = fun (b : β) (a : α) => f a b

@[reducible, inline]

def Function.dcomp {α : Sort u₁} {β : α → Sort u₂} {φ : {x : α} → β x → Sort u₃} (f : {x : α} → (y : β x) → φ y) (g : (x : α) → β x) (x : α) : φ (g x)

Composition of dependent functions: (f ∘' g) x = f (g x), where type of g x depends on x and type of f (g x) depends on x and g x.

Equations

• (f ∘' g) x = f (g x)

def Function.«term_∘'_» : Lean.TrailingParserDescr

Composition of dependent functions: (f ∘' g) x = f (g x), where type of g x depends on x and type of f (g x) depends on x and g x.

Equations

• Function.«term_∘'_» = Lean.ParserDescr.trailingNode `Function.«term_∘'_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘' ") (Lean.ParserDescr.cat `term 80))

@[reducible, inline]

abbrev Function.onFun {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → β → φ) (g : α → β) : α → α → φ

Given functions f : β → β → φ and g : α → β, produce a function α → α → φ that evaluates g on each argument, then applies f to the results. Can be used, e.g., to transfer a relation from β to α.

Equations

• Function.onFun f g x y = f (g x) (g y)

def Function.term_On_ : Lean.TrailingParserDescr

Given functions f : β → β → φ and g : α → β, produce a function α → α → φ that evaluates g on each argument, then applies f to the results. Can be used, e.g., to transfer a relation from β to α.

Equations

• Function.term_On_ = Lean.ParserDescr.trailingNode `Function.term_On_ 2 2 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " on ") (Lean.ParserDescr.cat `term 3))

@[reducible, inline]

abbrev Function.swap {α : Sort u₁} {β : Sort u₂} {φ : α → β → Sort u₃} (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) : φ x y

For a two-argument function f, swap f is the same function but taking the arguments in the reverse order. swap f y x = f x y.

Equations

• Function.swap f y x = f x y

theorem Function.swap_def {α : Sort u₁} {β : Sort u₂} {φ : α → β → Sort u₃} (f : (x : α) → (y : β) → φ x y) : swap f = fun (y : β) (x : α) => f x y

@[simp]

theorem Function.id_comp {α : Sort u₁} {β : Sort u₂} (f : α → β) : id ∘ f = f

@[simp]

theorem Function.comp_id {α : Sort u₁} {β : Sort u₂} (f : α → β) : f ∘ id = f

theorem Function.comp_assoc {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ g ∘ h

def Function.Injective {α : Sort u₁} {β : Sort u₂} (f : α → β) : Prop

A function f : α → β is called injective if f x = f y implies x = y.

Equations

• Function.Injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂

theorem Function.Injective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β → φ} {f : α → β} (hg : Injective g) (hf : Injective f) : Injective (g ∘ f)

def Function.Surjective {α : Sort u₁} {β : Sort u₂} (f : α → β) : Prop

A function f : α → β is called surjective if every b : β is equal to f a for some a : α.

Equations

• Function.Surjective f = ∀ (b : β), ∃ (a : α), f a = b

theorem Function.Surjective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β → φ} {f : α → β} (hg : Surjective g) (hf : Surjective f) : Surjective (g ∘ f)

def Function.Bijective {α : Sort u₁} {β : Sort u₂} (f : α → β) : Prop

A function is called bijective if it is both injective and surjective.

Equations

• Function.Bijective f = (Function.Injective f ∧ Function.Surjective f)

theorem Function.Bijective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : β → φ} {f : α → β} : Bijective g → Bijective f → Bijective (g ∘ f)

def Function.LeftInverse {α : Sort u₁} {β : Sort u₂} (g : β → α) (f : α → β) : Prop

LeftInverse g f means that g is a left inverse to f. That is, g ∘ f = id.

Equations

• Function.LeftInverse g f = ∀ (x : α), g (f x) = x

def Function.HasLeftInverse {α : Sort u₁} {β : Sort u₂} (f : α → β) : Prop

HasLeftInverse f means that f has an unspecified left inverse.

Equations

• Function.HasLeftInverse f = ∃ (finv : β → α), Function.LeftInverse finv f

def Function.RightInverse {α : Sort u₁} {β : Sort u₂} (g : β → α) (f : α → β) : Prop

RightInverse g f means that g is a right inverse to f. That is, f ∘ g = id.

Equations

• Function.RightInverse g f = Function.LeftInverse f g

def Function.HasRightInverse {α : Sort u₁} {β : Sort u₂} (f : α → β) : Prop

HasRightInverse f means that f has an unspecified right inverse.

Equations

• Function.HasRightInverse f = ∃ (finv : β → α), Function.RightInverse finv f

theorem Function.LeftInverse.injective {α : Sort u₁} {β : Sort u₂} {g : β → α} {f : α → β} : LeftInverse g f → Injective f

theorem Function.HasLeftInverse.injective {α : Sort u₁} {β : Sort u₂} {f : α → β} : HasLeftInverse f → Injective f

theorem Function.rightInverse_of_injective_of_leftInverse {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} (injf : Injective f) (lfg : LeftInverse f g) : RightInverse f g

theorem Function.RightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} (h : RightInverse g f) : Surjective f

theorem Function.HasRightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : α → β} : HasRightInverse f → Surjective f

theorem Function.leftInverse_of_surjective_of_rightInverse {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α} (surjf : Surjective f) (rfg : RightInverse f g) : LeftInverse f g

theorem Function.injective_id {α : Sort u₁} : Injective id

theorem Function.surjective_id {α : Sort u₁} : Surjective id

theorem Function.bijective_id {α : Sort u₁} : Bijective id

theorem Function.Injective.eq_iff {α : Sort u₁} {β : Sort u₂} {f : α → β} (I : Injective f) {a b : α} : f a = f b ↔ a = b

theorem Function.Injective.beq_eq {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {f : α → β} (I : Injective f) {a b : α} : (f a == f b) = (a == b)

theorem Function.Injective.eq_iff' {α : Sort u₁} {β : Sort u₂} {f : α → β} (I : Injective f) {a b : α} {c : β} (h : f b = c) : f a = c ↔ a = b

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

theorem Function.Injective.ne_iff {α : Sort u₁} {β : Sort u₂} {f : α → β} (hf : Injective f) {x y : α} : f x ≠ f y ↔ x ≠ y

theorem Function.Injective.ne_iff' {α : Sort u₁} {β : Sort u₂} {f : α → β} (hf : Injective f) {x y : α} {z : β} (h : f y = z) : f x ≠ z ↔ x ≠ y

theorem Function.LeftInverse.id {α : Type u₁} {β : Type u₂} {g : β → α} {f : α → β} (h : LeftInverse g f) : g ∘ f = id

theorem Function.RightInverse.id {α : Type u₁} {β : Type u₂} {g : β → α} {f : α → β} (h : RightInverse g f) : f ∘ g = id

def Function.IsFixedPt {α : Type u₁} (f : α → α) (x : α) : Prop

A point x is a fixed point of f : α → α if f x = x.

Equations

• Function.IsFixedPt f x = (f x = x)

def Pi.map {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} (f : (i : ι) → α i → β i) : ((i : ι) → α i) → (i : ι) → β i

Sends a dependent function a : ∀ i, α i to a dependent function Pi.map f a : ∀ i, β i by applying f i to i-th component.

Equations

• Pi.map f a i = f i (a i)

@[simp]

theorem Pi.map_apply {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} (f : (i : ι) → α i → β i) (a : (i : ι) → α i) (i : ι) : Pi.map f a i = f i (a i)