Lately I encountered the definition of proper group:
A $G$-action on $X$ is called proper if the function $f:(g,x)\mapsto (g\cdot x, x)$ is proper, i.e. for any compact set $U\subset X\times X$, the preimage $f^{-1}(U)$ is compact.
But I have no clue how to check this on concrete examples.
For example consider $\mathbb Z \times \mathbb R \to \mathbb R$, $(n,x)\mapsto x+n$.
Its clear that for any $n\in \mathbb Z$, $n^{-1}\cdot[0,1]=[-1,1]$ and so $$f^{-1}([0,1]) = \bigcup_{n\in \mathbb Z} \{n\}\times [-n,-n+1],$$ but this is still an infinite union of compact sets. Also, even if I show this, it does not really help me. It's not like in the case of continuity that it suffices to consider balls.
Another example which should be easy to check is the action of $GL(V)$ on the vector space $V$, (for symplicity $V = \mathbb R^2$).
So here is my question: Could you provide me with some examples of proper discontinuous group actions and most importantly how to check this property?
Edit: The first answer is based on the Poincare Polyhedron Theorem which looks very useful. However, i would also like to see a more direct approach worling with the definitions.
In the case of discrete groups acting on the spaces $\mathbb R^n$, $\mathbb H^n$, or $\mathbb S^n$ (Euclidean spaces, hyperbolic spaces, and spheres), the Poincaré polyhedron theorem is a very nice tool for verifying properness.
There are many features of the Poincare Polyhedron Theorem that I cannot go into here, and for the general statement it's probably best to go and read about it. Ratcliffe's "Foundations of hyperbolic manifolds" has the statement.
What I'll do is just to give a very few simple examples.
First example: Start with the square $Q = [0,1] \times [0,1] \subset \mathbb R^2$. Consider the two isometries $f,g : \mathbb R^2 \to \mathbb R^2$ given by $f(x,y)=(x+1,y)$ and $g(x,y)=(x,y+1)$.
The two isometries $f$ and $g$ form a set of "side pairing" isometries of the square $Q$:
Next notice that at each of the four corners of $Q$ one can verify a "corner cycle" condition. For instance, the corner cycle condition at the corner $(0,0)$ goes like this:
One can visualize the squares $Q$, $Q'$, $Q''$, and $Q'''$ as forming a cycle of squares around the vertex $(0,0)$, non-overlapping except that two consecutive squares in this cycle intersect along a common edge, and two nonconsecutive squares intersect at $(0,0)$.
From that corner cycle, one obtains a relator in the group generated by $f$ and $g$, namely $g f g^{-1} f^{-1}$ is equal to the identity isometry.
The Poincare Polyhedron Theorem says that if you have a polyhedron and a set of side pairing isometries which satisfy appropriate corner cycle conditions, then the group generated by those isometries acts properly, with respect to the discrete topology on that group.
There are further conclusions to be made as well. First, the corner cycles give you defining relators, and so with the generators you end up with an actual presentation for the group. Also (with some further hypotheses in the case of $\mathbb H^2$) the given polyhedron is a fundamental domain for the action.
In the example I have described, the generators $f$ and $g$, and every relator is a commutator such as the one $g f g^{-1} f^{-1}$ shown, and so the group is isomorphic to $\mathbb Z^2$.
Second example: In your $1$-dimensional example, the polyhedron is $[0,1]$ and $g(x)=x+1$ is a set of side pairing isometries all by itself. There are no corners in dimension $0$, and hence no relators. The group generated by $g$ is therefore infinite cyclic, and it acts properly on $\mathbb R$.
Third example: Here's a brief higher dimensional example. Start with the cube $C = [0,1] \times [0,1] \times [0,1]$.
The cube has six sides --- i.e. six codimension 1 faces. What I will take for the side pairing isometries are three translations that pair opposite sides of the cube. This exhibits that for general dimension $n$, the general concept of "side pairing isometries" is formulated using codimension-1 faces of the polyhedron.
The cube has eight edges --- i.e. eight codimension 1 faces. There is a "corner cycle" condition associated to each of these eight edges, and in this case they all have the form of a commutator of two out of the three side pairing isometries. This exhibits that for general dimension $n$, the general concept of "corner cycles" is formulated using codimension-2 faces of the polyhedron.
The group generated by the three side pairings is $\mathbb Z^3$ and acts properly on $\mathbb R^3$.