Theorems · Definition · algebraic topology

IsEvenlyCovered

{E : Type u_1} →
  {X : Type u_2} →
    [TopologicalSpace E] → [TopologicalSpace X] → (E → X) → X → (I : Type u_3) → [TopologicalSpace I] → Prop

A point x : X is evenly covered by f : E → X if x has an evenly covered neighborhood. Remark: DiscreteTopology I ∧ ∃ Trivialization I f, x ∈ t.baseSet would be a simpler definition, but unfortunately it does not work if E is nonempty but nonetheless f has empty fibers over s. If OpenPartialHomeomorph could be refactored to work with an empty space and a nonempty space while preserving the APIs, we could switch back to the definition.

Defined in

Mathlib.Topology.Covering.Basic

Cited by

22 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace