Functional: ∀x ∈ P, there exists at most one element of Q, written f(x), such that (x, f(x)) ∈ f

Total function: ∀x ∈ P, f(x) is uniquely defined such that (x, f(x)) ∈ f

Injective: ∀x,y ∈ P, if f(x) = f(y), then x = y

Surjective: ∀y ∈ Q, ∃x ∈ P such that f(x) = y

Transitive: ∀x,y,z ∈ P, if x≤y and y≤z then x≤z

Reflexive: ∀x ∈ P, x≤x

Antisymmetric: ∀x,y ∈ P, if x≤y and y≤x then x=y

A preorder: P is transitive and reflexive

A partial order: P is a preorder and antisymmetric

A total order: P is a partial order and ∀x,y ∈ P, x ≤ y or y ≤ x

Has meets: ∀x,y ∈ P, ∃ x∧y ∈ P such that x∧y ≤ x, x∧y ≤ y, and ∀z ∈ P, if z ≤ x and z ≤ y, then z ≤ x∧y.

Has joins: ∀x,y ∈ P, ∃ x∨y ∈ P such that x ≤ x∨y, y ≤ x∨y, and ∀z ∈ P, if x ≤ z and y ≤ z, then x∨y ≤ z.

Transitive: ∀x,y,z ∈ P, if x≤y and y≤z then x≤z

Reflexive: ∀x ∈ P, x≤x

Antisymmetric: ∀x,y ∈ P, if x≤y and y≤x then x=y

A preorder: P is transitive and reflexive

A partial order: P is a preorder and antisymmetric

A total order: P is a partial order and ∀x,y ∈ P, x ≤ y or y ≤ x

Has meets: ∀x,y ∈ P, ∃ x∧y ∈ P such that x∧y ≤ x, x∧y ≤ y, and ∀z ∈ P, if z ≤ x and z ≤ y, then z ≤ x∧y.

Has joins: ∀x,y ∈ P, ∃ x∨y ∈ P such that x ≤ x∨y, y ≤ x∨y, and ∀z ∈ P, if x ≤ z and y ≤ z, then x∨y ≤ z.