Theorems · Inductive type · algebraic topology

IsQuotientCoveringMap

{E : Type u_1} →
  {X : Type u_2} →
    [TopologicalSpace E] → [TopologicalSpace X] → (E → X) → (G : Type u_3) → [inst : Group G] → [MulAction G E] → Prop

A function from a topological space E with an action by a discrete group to another topological space X is a quotient covering map if it is a quotient map, the action is continuous and transitive on fibers, and every point of E has a neighborhood whose translates by the group elements are pairwise disjoint.

Defined in

Mathlib.Topology.Covering.Quotient

Cited by

53 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceGroupMulAction