# Logic formulas concerning functions

A relation R between two sets A and B is a functional relation iff, for all x in A, there are y and z in B, such that (x,y) ∈ R and (x,z) ∈ R implies y = z.

> ∀x ∈ A. ∃y∃y' ∈ B. \[ (x,y) ∈ F ∧ (x,y') ∈ F ] -> y = y'

A partial function is a triple f =  where A and B are arbitrary, possibly empty, sets, and F is a functional, possibly empty, relation between A and B, called _the graph of `f`_.

A function `f: A → B` is **injective** (one to one) iff, ∀x∀y ∈ A. f(x) = f(y) implies that x = y. (dom = ran < cod)

> f:A→B is injective <=> ∀a∀a' ∈ A. \[ f(a) = f(a') ] -> a = a'

A function f: A → B is **surjective** (onto) iff, for all y ∈ B, there is some x ∈ A such that f(x) = y. Equivalently, the range of f is the set B. (dom >= cod = ran)

> f:A→B is surjective <=> ∀y ∈ B. ∃x ∈ A. f(x) = y

A function is **bijective** (1:1 correspondence) iff it is both injective and surjective. (dom = cod = ran)

* injection : |dom = ran| < |cod|
* surjection: |dom| > |ran = cod|
* bijection : |dom| = |ran| = |cod|

A partial function doesn't have the entire domain engaged. With partial functions, injection cannot be distinguished from bijection. A partial surjection is also possible.
