Theorems · Theorem · algebraic topology

isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul

∀ {E : Type u_1} [inst : TopologicalSpace E] {G : Type u_3} [inst_1 : Group G] [inst_2 : MulAction G E]
  [ContinuousConstSMul G E] [ProperlyDiscontinuousSMul G E] [LocallyCompactSpace E] [T2Space E],
  IsCoveringMapOn (Quotient.mk (MulAction.orbitRel G E))
    (Quotient.mk (MulAction.orbitRel G E) '' {e | MulAction.stabilizer G e = ⊥})

Defined in

Mathlib.Topology.Covering.Quotient

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceGroupMulActionContinuousConstSMulProperlyDiscontinuousSMulLocallyCompactSpaceT2Space