命題
G を局所コンパクト空間 X に固有に作用(>>473)する局所コンパクト群とする。
X/G を X の G による軌道空間(過去スレ004の390)とする。
p: X → X/G を標準射とする。
L を X/G の任意のコンパクト集合とする。

このとき、X のコンパクト集合 K があり、p(K) = L となる。

証明
任意の y ∈ L に対して f^(-1)(y) は空でない。
よって選択公理より τ(y) ∈ f^(-1)(y) となる選択関数 τ が存在する。
τ(y) のコンパクト近傍を V(y) と書く。
>>487の証明で示したように p は開写像だから p(V(y)) は
y のコンパクト近傍である。
L はコンパクトだから、L の有限個の点 y_1, ..., y_n があり、
L ⊂ ∪f(V(y_i)), i = 1, ..., n となる。
M = ∪V(y_i) とおく。
L ⊂ f(M) である。

K = M ∩ f^(-1)(L) とおく。
f^(-1)(L) は閉集合だから K はコンパクトである。
明らかに f(K) ⊂ L である。
L ⊂ f(M) だから L の任意の元 y に対して z = f(x) となる x ∈ M がある。
x ∈ f^(-1)(L) だから x ∈ K である。
よって、L ⊂ f(K) となって f(K) = L である。
証明終