Function Images

We define the image of a given function as all elements that can be reached from a given domain. We provide a list and a set version.

def Function.imageSet {α : Type u} {β : Type v} (f : α → β) (A : Set α) : Set β

The image of a function for a given domain set.

Equations

• Function.imageSet f A = A.map f

theorem Function.mapping_mem_imageSet_of_mem {α : Type u} {β : Type v} {f : α → β} {domain : Set α} {a : α} : a ∈ domain → f a ∈ imageSet f domain

The mapping of each domain element occurs in the image.

def Function.imageList {α : Type u} {β : Type v} [DecidableEq β] (f : α → β) (l : List α) : List β

The image of a function for a given domain list.

Equations

• Function.imageList f l = (List.map f l).eraseDupsKeepRight

theorem Function.mapping_mem_imageList_of_mem {α : Type u} {β : Type v} [DecidableEq β] {f : α → β} {domain : List α} {a : α} : a ∈ domain → f a ∈ imageList f domain

The mapping of each domain element occurs in the image.

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

The image has no duplicates.

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

The image has at most as many elements as the domain.