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 CustomBasicDatastructures.Function.imageSet {α : Type u} {β : Type v} (f : α → β) (A : Set α) : Set β

The image of a function for a given domain set.

Equations

• CustomBasicDatastructures.Function.imageSet f A = A.map f

theorem CustomBasicDatastructures.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 CustomBasicDatastructures.Function.imageList {α : Type u} {β : Type v} [DecidableEq β] (f : α → β) (l : List α) : List β

The image of a function for a given domain list.

Equations

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

theorem CustomBasicDatastructures.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 CustomBasicDatastructures.Function.nodup_imageList {α : Type u} {β : Type v} [DecidableEq β] {f : α → β} {domain : List α} : (imageList f domain).Nodup

The image has no duplicates.

theorem CustomBasicDatastructures.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.