Fundamental group of the sphere

Stream: Is there code for X?

[Adrian]

Is there a proof that the fundamental group of the two dimensional sphere is the trivial group?

[Jireh Loreaux]

I don't believe so, as the import chain only has:

Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup →
Mathlib.Topology.Homotopy.HomotopyGroup →
Mathlib

[Michael Rothgang]

This result (perhaps for the n-sphere, for any $n\geq 2$) would certainly be a welcome addition to mathlib!

[Yury G. Kudryashov]

The only instance for SimplyConnected is for contractible spaces.

[Yury G. Kudryashov]

What's the easiest argument here? Prove some exact sequence? Or find a smooth curve homotopic to a given continuous curve, deduce that the range is not the whole sphere, then apply stereographic projection?

[Jz Pan]

Yury G. Kudryashov said:

What's the easiest argument here? Prove some exact sequence? Or find a smooth curve homotopic to a given continuous curve, deduce that the range is not the whole sphere, then apply stereographic projection?

I think the textbook way to prove that $\pi_1(S^n), n\geq 2$ is trivial is using https://en.wikipedia.org/wiki/Seifert%E2%80%93Van_Kampen_theorem.