# Function (abjections)

f : A -> B

f(a) = b

graph(f) = { (a, f(b)) | a ∈ A }

∀a ∈ A. ∃b ∈ B. f(a) = b ∀a∃b.\[a ∈ A ⋀ b ∈ B -> f(a) = b]

∀aa' ∈ A. f(a) = f(a') <=> a = a' ∀aa'.\[(a ∈ A ⋀ a' ∈ A) -> (f(a) = f(a') <=> a = a')]

∀b ∈ B. ∃a ∈ A. f(a) = b

∀b∃a ∈ A. f⁻¹(b) = a <=> f(a) = b

∀b ∈ B. ∃a ∈ A. f⁻¹(b) = a <=> f(a) = b

A total function (or just function) is a relation where each member of the domain is associated with (at most) one element of the codomain.

Properties:

* all elements of the domain are engaged
* some elements of the codomain are engaged
* a distinct domain element, `x`, cannot be associated with more than one codomain element:

A function is a special relation `R` between two sets `A` and `B`, consisting of a set of ordered pairs `(a,b)` where `a ∈ A` and `b ∈ B`

R ⊆ A ⨯ B

denoted `f : A -> B`, and

f : A -> B graph(f) = { (x, y₁), (x, y₁) }

f(x) = y ⋀ f(x) = z ⋀ y ≠ z

in non-injective and non-surjective if