Function

Def: A function f is a set of ordered pairs satisfying
((x,y1)∈f ∧ (x,y2)∈f) ⇒ (y1=y2)

Note: Each x is mapped by f to at most one value of y.

Note: ∅ is a function.

Note: if f is finite then
f is a function ⇔ |f|=|dom(f)|
(where for any finite set s, |s| denotes the number of elements in s)

Note: ∀d, f is a function ⇒ restrict(f,d) is a function

Note: f, g are functions ⇒ f∘g is a function.

Dot notation: Let f be a function, and x∈dom(f). Then f.x ∈ image(f) denotes the value mapped by x, and satisfies (x,f.x)∈f.

Def: A function f is injective if
(x1,y)∈f ∧ (x2,y)∈f ⇒ x1=x2

Note: Injectivity mirrors the definition of a function with the roles of x and y exchanged.

Note: f^-1 is a function ⇔ f is injective.

Note: if f finite then (f is injective ⇔ |dom(f)| = |image(f)| ).

Note: Many texts define a function as having a codomain which might not equal its image. Since we do not, it is meaningless to ask whether a function is surjective. Therefore injectivity and bijectivity are synonymous.

Note: Since functions have no concept of a codomain, a function is identified with a set of ordered pairs and nothing more. It follows that two functions are equal if and only if they are equal as sets of ordered pairs. This is the reason for dropping the notion of a codomain. Many texts refer to the set of ordered pairs as the graph of the function, in order that the function may have a codomain defined.