Theorems · Inductive type · algebraic topology

IsAddQuotientCoveringMap

{E : Type u_1} →
  {X : Type u_2} →
    [TopologicalSpace E] →
      [TopologicalSpace X] → (E → X) → (G : Type u_4) → [inst : AddGroup G] → [AddAction 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

42 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceAddGroupAddAction