Theorems · Theorem · algebraic topology

IsCoveringMap.existsUnique_continuousMap_lifts

∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X},
  IsCoveringMap p →
    ∀ [SimplyConnectedSpace A] [LocallyPathConnectedSpace A] (f : C(A, X)) (a₀ : A) (e₀ : E),
      p e₀ = f a₀ → ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

A continuous map f from a simply-connected, locally path-connected space A to another space X lifts uniquely through a covering map p : E → X, after specifying any lift e₀ : E of any point a₀ : A.

Defined in

Mathlib.Topology.Homotopy.Lifting

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceSimplyConnectedSpaceLocallyPathConnectedSpace