Corollary 3

If S is finite, σ(W) is a discrete subgroup of \mathbf{GL}(E) provided with its canonical Lie group structure; similarly, σ(W) is a discrete subgroup of* \mathbf{GL}(E^*) .

Let x* ∈ C. The set U of g ∈ \mathbf{GL}(E^*) such that g(x*) ∈ C is a neighbourhood of the identity element in \mathbf{GL}(E^*); by the theorem,

thus, σ*(W) is a discrete subgroup of \mathbf{GL}(E^*). By transport of structure, it follows that σ(W) is discrete in \mathbf{GL}(E).

Proof of Theorem 1.

If $w \in W$, denote by $l(w)$ the length of $w$ with respect to $S$ (Chap. IV, § 1, no. 1).

We are going to prove the following assertions, where $n$ denotes an integer $\geqslant 0$:

(P_n) Let $w \in W$, with $l(w) = n$, and $s \in S$. Then: either $w(C) \subset A_s$; or $w(C) \subset s(A_s)$ and $l(sw) = l(w) - 1$.

(Q_n) Let $w \in W$, with $l(w) = n$, and $s, s' \in S, s \neq s'$. Let $W_{s,s'}$ be the subgroup of $W$ generated by $s$ and $s'$. There exists $u \in W_{s,s'}$ such that

These assertions are trivial for $n = 0$. We prove them by induction on $n$, according to the scheme

Proof that $((P_n) \text{ and } (Q_n)) \Longrightarrow (P_{n+1})$.

Let $w \in W$, with $l(w) = n + 1$, and $s \in S$. We can write $w$ in the form $w = s'w'$ with $s' \in S$ and $l(w') = n$. If $s' = s$, $(P_n)$ applied to $w'$ shows that $w'(C) \subset A_s$, hence $w(C) \subset s(A_s)$ and $l(sw) = l(w') = l(w) - 1$. If $s' \neq s$, $(Q_n)$ applied to $w'$ shows that there exists $u \in W_{s,s'}$ such that

We have $w(C) = s'w'(C) \subset s'u(A_s \cap A_{s'})$.