Hopf problem: foundations · core 4 #
Supporting definitions and proofs for this stage of the six-sphere construction.
noncomputable def
Mathoverflow1973.homeomorphFundamentalGroupEquiv
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
(e : X ≃ₜ Y)
(x : X)
:
The multiplicative equivalence on fundamental groups induced by a homeomorphism.
Equations
- One or more equations did not get rendered due to their size.