Hopf problem: foundations · invariant subset quotient #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.InvariantSubsetQuotient.isClosed_image
{M : Type u_1}
{Q : Type u_2}
{q : M → Q}
{S : Set M}
[TopologicalSpace M]
[TopologicalSpace Q]
{G : Type u_3}
[Group G]
[MulAction G M]
[MulAction G ↑S]
(hq : IsQuotientCoveringMap q G)
(hcompat : ∀ (g : G) (x : ↑S), ↑(g • x) = g • ↑x)
(hS : IsClosed S)
: