Corollary 1
Tag 0BKZ, permanent. Cite it as [Bourbaki, Tag 0BKZ].
General Topology, chapter III, § 4. Groups operating properly on a topological space; compact ness in topological groups and spaces with operators
Under the hypotheses of Proposition 2, X is compact (resp. locally compact) if and only if X/K is compact (resp. locally compact).
This follows from the fact that the canonical mapping X → X/K is proper, in view of Proposition 9 of Chapter I, § 10, no. 4.
Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.