Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 01:02 3600b621

View on Github →

feat(topology/homotopy): define nth homotopy group πₙ (without the group instance) (#14724) This pull request adds:

  • definition of the nth homotopy group π n x
  • proof of π 0 x ≃ zeroth_homotopy X where x:X
  • proof of π 1 x ≃ path.homotopic.quotient x x

Estimated changes

added def cube.boundary
added theorem cube.head.continuous
added def cube.head
added theorem cube.one_char
added theorem cube.proj_continuous
added def cube.tail
added def cube
added def gen_loop.const
added theorem gen_loop.ext
added theorem gen_loop.mk_apply
added structure gen_loop
added def homotopy_group