Hopf problem: threefold ยท special periods 11 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.SpecialPeriods.Threefold.PiOne.mapOfEq_eq_one_of_map_eq_one_mo1973_26295
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
(f : C(X, Y))
{x : X}
{y : Y}
(e : f x = y)
(g : FundamentalGroup X x)
(h : (FundamentalGroup.map f x) g = 1)
: