Expansive homeomorphism

In mathematics, the notion of expansivity formalizes the notion of points moving away from one another under the action of an iterated function. The idea of expansivity is fairly rigid, as the definition of positive expansivity, below, as well as the Schwarz–Ahlfors–Pick theorem demonstrate.
Definition.
If formula_1 is a metric space, a homeomorphism formula_2 is said to be expansive if there is a constant 
called the expansivity constant, such that for every pair of points formula_4 in formula_5 there is an integer formula_6 such that 
Note that in this definition, formula_6 can be positive or negative, and so formula_9 may be expansive in the forward or backward directions.
The space formula_5 is often assumed to be compact, since under that assumption expansivity is a topological property; i.e. if formula_11 is any other metric generating the same topology as formula_12, and if formula_9 is expansive in formula_1, then formula_9 is expansive in formula_16 (possibly with a different expansivity constant).
If 
is a continuous map, we say that formula_5 is positively expansive (or forward expansive) if there is a 
such that, for any formula_4 in formula_5, there is an formula_22 such that formula_23.
Theorem of uniform expansivity.
Given "f" an expansive homeomorphism of a compact metric space, the theorem of uniform expansivity states that for every formula_24 and formula_25 there is an formula_26 such that for each pair formula_27 of points of formula_5 such that formula_29, there is an formula_30 with formula_31 such that 
where formula_33 is the expansivity constant of formula_9 (proof).
Discussion.
Positive expansivity is much stronger than expansivity. In fact, one can prove that if formula_5 is compact and formula_9 is a positively
expansive homeomorphism, then formula_5 is finite (proof).