Theorems · Theorem · algebraic topology

IsCoveringMapOn.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} [SimplyConnectedSpace A] [LocallyPathConnectedSpace A] {s : Set X},
  IsCoveringMapOn p s →
    ∀ (f : C(A, X)) {a₀ : A} {e₀ : E}, p e₀ = f a₀ → (∀ (a : A), f a ∈ s) → ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f

A version of IsCoveringMap.existsUnique_continuousMap_lifts for maps that are covering on a subset of the codomain. Let p be a covering map on s. Let f be a continuous map with a simply connected locally path connected domain such that all values of f belong to s. Given a point a₀ in the domain of f and a lift e₀ of f a₀ along p, there exists a unique lift F of f along p such that F a₀ = e₀.

Defined in

Mathlib.Topology.Homotopy.Lifting

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceSimplyConnectedSpaceLocallyPathConnectedSpace