# Right tight function restriction expression

## Definition

### Symbol-free definition

A function restriction expression is said to be right tight if the right side cannot be made any stronger for the same choice of left side.

### Definition with symbols

A function restriction expression $a \to b$ is said to be right tight if given $c \le b$ such that $a \to c = a \to b$, we have $c = b$.

## Facts

For any given choice of left side, there is a unique choice of right side that makes the expression right tight. The operation of transforming an arbitrary function restriction expression, to the one with this right side, is termed right tightening.