# nLab inequality relation

foundations

## Removing axioms

In constructive mathematics, an inequality relation is a binary relation that is irreflexive and symmetric. An inequality relation is often denoted ‘$\ne$’ (infix) or a variation.

Although this concept is nontrivial in classical mathematics, one does not usually run across it there; this is because one is usually interested in tight inequalities (see below), and excluded middle shows that the only tight inequality (on a given set) is the denial inequality (the negation of equality).

The term ‘inequality relation’ is often shortened to ‘inequality’, but it should not be confused with order relations (the sort typically denoted ‘$\le$’ or a variation). Sometimes ‘inequation’ is used for a statement containing an inequality relation (much as ‘equation’ is used for a statement containing an equality relation), leaving ‘inequality’ to mean a statement containing an order relation).

Specific types of inequality relations include: