Flexible Injectivity and Surjectivity

We define what it means for a function to be injective or surjective restricted to a given domain and image, given as either a list or set. Intuitively, results involving the list versions most likely have an implicit requirement for domain and image being finite whereas results stated for the set version do not have this requirement. In this sense the set results can be seen as most general. The list and set definitions are also shown to be equivalent in cases where the domains and images can be converted between lists and sets.

We found the approach of stating domains and images explicitely more suitable than using Function.Injective and Function.Surjective because this would require us to consider appropriate subtypes and also since there barely seem to be theorems in the standard library (outside Mathlib).

def Function.injectiveSet {α : Type u} {β : Type v} (f : α → β) (domain : Set α) : Prop

A function is injective on a given domain set if for each two elements of the given domain, the mapping of both elements being the same implies the elements being the same.

Equations

• Function.injectiveSet f domain = ∀ (a a' : α), a ∈ domain → a' ∈ domain → f a = f a' → a = a'

def Function.surjectiveSet {α : Type u} {β : Type v} (f : α → β) (domain : Set α) (image : Set β) : Prop

A function is surjective on a given domain set and image set if for each element of the image, there exists an element in the domain that maps to the desired image element.

Equations

• Function.surjectiveSet f domain image = ∀ (b : β), b ∈ image → ∃ (a : α), a ∈ domain ∧ f a = b

def Function.closedSet {α : Type u} (f : α → α) (domain : Set α) : Prop

A function over a type is closed for a given domain if the image of every domain element is mapped to an element that is again in the domain.

Equations

• Function.closedSet f domain = ∀ (a : α), a ∈ domain → f a ∈ domain

theorem Function.injectiveSet_of_injectiveSet_of_subset {α : Type u} {β : Type v} {f : α → β} {domain : Set α} : injectiveSet f domain → ∀ (domain' : Set α), domain' ⊆ domain → injectiveSet f domain'

If a mapping is injective for a domain, then the same holds for any subset of the domain.

theorem Function.surjectiveSet_of_surjectiveSet_of_superset {α : Type u} {β : Type v} {f : α → β} {domain : Set α} {image : Set β} : surjectiveSet f domain image → ∀ (domain' : Set α), domain ⊆ domain' → surjectiveSet f domain' image

If a mapping is surjective for a domain and image, then the same holds for any superset of the domain.

theorem Function.injectiveSet_of_injectiveSet_compose {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {domain : Set α} : injectiveSet (g ∘ f) domain → injectiveSet f domain

If the composition of two mappings is injective, then the first one must be injective.

theorem Function.surjectiveSet_of_surjectiveSet_compose {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {domain : Set α} {image : Set γ} : surjectiveSet (g ∘ f) domain image → surjectiveSet g (imageSet f domain) image

If the composition of two mappings is surjective for a domain and image, then the second one must be surjective on the same image and the domain that is the image of the first function.

theorem Function.surjective_on_own_imageSet {α : Type u} {β : Type v} (f : α → β) (domain : Set α) : surjectiveSet f domain (imageSet f domain)

Every mapping is always surjective on its own imageSet.

theorem Function.imageSet_contained_of_closed {α : Type u} {f : α → α} {domain : Set α} (closed : closedSet f domain) : imageSet f domain ⊆ domain

If a mapping is closed, then its image is fully contained in its domain.

theorem Function.surjective_on_target_iff_all_in_imageSet {α : Type u} {β : Type v} {f : α → β} {domain : Set α} {target_image : Set β} : surjectiveSet f domain target_image ↔ ∀ (b : β), b ∈ target_image → b ∈ imageSet f domain

A mapping is surjective on a given domain and image if and only if the given image is contained in the actual image of the mapping.

def Function.injectiveList {α : Type u} {β : Type v} (f : α → β) (domain : List α) : Prop

A function is injective on a given domain list if for each two elements of the given domain, the mapping of both elements being the same implies the elements being the same.

Equations

• Function.injectiveList f domain = ∀ (a a' : α), a ∈ domain → a' ∈ domain → f a = f a' → a = a'

def Function.surjectiveList {α : Type u} {β : Type v} (f : α → β) (domain : List α) (image : List β) : Prop

A function is surjective on a given domain list and image list if for each element of the image, there exists an element in the domain that maps to the desired image element.

Equations

• Function.surjectiveList f domain image = ∀ (b : β), b ∈ image → ∃ (a : α), a ∈ domain ∧ f a = b

def Function.closedList {α : Type u} (f : α → α) (domain : List α) : Prop

A function over a type is closed for a given domain if the image of every domain element is mapped to an element that is again in the domain.

Equations

• Function.closedList f domain = ∀ (a : α), a ∈ domain → f a ∈ domain

theorem Function.injective_set_list_equiv {α : Type u} {β : Type v} {f : α → β} {domain_set : Set α} {domain_list : List α} (eq : ∀ (e : α), e ∈ domain_set ↔ e ∈ domain_list) : injectiveSet f domain_set ↔ injectiveList f domain_list

The injectivity definitions for set and list are interchangeable.

theorem Function.surjective_set_list_equiv {α : Type u} {β : Type v} {f : α → β} {domain_set : Set α} {domain_list : List α} (eq_domain : ∀ (e : α), e ∈ domain_set ↔ e ∈ domain_list) {image_set : Set β} {image_list : List β} (eq_image : ∀ (e : β), e ∈ image_set ↔ e ∈ image_list) : surjectiveSet f domain_set image_set ↔ surjectiveList f domain_list image_list

The surjectivity definitions for set and list are interchangeable.

theorem Function.injectiveList_cons {α : Type u} {β : Type v} {f : α → β} {hd : α} {tl : List α} : injectiveList f (hd :: tl) → injectiveList f tl

If a mapping is injective on a domain of the form hd::tl, then it is injective on tl.

theorem Function.surjectiveList_cons {α : Type u} {β : Type v} {f : α → β} {hd : α} {tl : List α} {image : List β} : surjectiveList f tl image → surjectiveList f (hd :: tl) image

If a mapping is surjective on a domain tl, then it is surjective on any domain hd::tl.

theorem Function.surjective_on_own_imageList {α : Type u} {β : Type v} [DecidableEq β] (f : α → β) (domain : List α) : surjectiveList f domain (imageList f domain)

Every mapping is always surjective on its own imageList.

theorem Function.imageList_contained_of_closed {α : Type u} [DecidableEq α] {f : α → α} {domain : List α} (closed : closedList f domain) : imageList f domain ⊆ domain

If a mapping is closed, then its image is fully contained in its domain.

theorem Function.injectiveList_iff_length_imageList_eq_of_nodup {α : Type u} {β : Type v} [DecidableEq β] {f : α → β} {domain : List α} (nodup : domain.Nodup) : injectiveList f domain ↔ (imageList f domain).length = domain.length

Given a mapping and a domain list without duplicates, the mapping in injective on the domain if and only if the imageList contains the same number of elements as the domain.

theorem Function.surjective_on_target_iff_all_in_imageList {α : Type u} {β : Type v} [DecidableEq β] {f : α → β} {domain : List α} {target_image : List β} : surjectiveList f domain target_image ↔ ∀ (b : β), b ∈ target_image → b ∈ imageList f domain

A mapping is surjective on a given domain and image if and only if the given image is contained in the actual image of the mapping.

theorem Function.injective_of_surjective_of_nodup {α : Type u} [DecidableEq α] {f : α → α} {l : List α} (nodup : l.Nodup) : surjectiveList f l l → injectiveList f l

Given a single list without duplicates that represents both domain and image, if a mapping is surjective, then it is injective.

theorem Function.injective_iff_surjective_of_nodup_of_closed {α : Type u} [DecidableEq α] {f : α → α} {l : List α} (nodup : l.Nodup) (closed : closedList f l) : injectiveList f l ↔ surjectiveList f l l

Given a single list without duplicates that represents both domain and image, if a mapping closed on the list, then the mapping is injective if and only if it is surjective.

theorem Function.closed_of_injective_of_surjective_of_nodup {α : Type u} [DecidableEq α] {f : α → α} {l : List α} (nodup : l.Nodup) : injectiveList f l → surjectiveList f l l → closedList f l

Given a single list without duplicates that represents both domain and image, if a mapping both injective and surjective, then is must be closed on the list.