Hopf problem: foundations · split group extension #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.fundamentalGroup_map_surjective_at_of_pathConnected
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
[PathConnectedSpace X]
(f : C(X, Y))
(x₀ x₁ : X)
(hf : Function.Surjective ⇑(FundamentalGroup.map f x₀))
: