Commit 2023-05-30 23:49 ff4f0707

View on Github →

feat: port Topology.Homotopy.HomotopyGroup (#4485)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

added def ContinuousMap.constPi

added def ContinuousMap.prodSwap

Modified Mathlib/Topology/Homotopy/Basic.lean

added def ContinuousMap.Homotopy.compContinuousMap

added theorem ContinuousMap.homotopicRel_empty

Created Mathlib/Topology/Homotopy/HomotopyGroup.lean

added def Cube.boundary

added theorem Cube.boundary_one

added theorem Cube.boundary_zero

added theorem Cube.head.continuous

added def Cube.head

added theorem Cube.mem_boundary

added theorem Cube.one_char

added theorem Cube.one_mem_boundary

added theorem Cube.proj_continuous

added def Cube.tail

added theorem Cube.zero_mem_boundary

added def Cube

added theorem GenLoop.Homotopic.equiv

added theorem GenLoop.Homotopic.refl

added def GenLoop.Homotopic

added def GenLoop.const

added def GenLoop.diagonal

added theorem GenLoop.ext

added theorem GenLoop.mk_apply

added theorem GenLoop.toContinuousMap_apply

added structure GenLoop

added def HomotopyGroup

added def genLoopOneEquivPathSelf

added theorem genLoopOneEquivPathSelf_homotopic_iff

added theorem genLoopOneEquivPathSelf_symm_homotopic_iff

added def genLoopZeroEquiv

added theorem homotopic_genLoopZeroEquiv_symm_iff

added theorem joined_genLoopZeroEquiv_iff

added def pi0EquivPathComponents

added def pi1EquivFundamentalGroup

Modified Mathlib/Topology/Homotopy/Path.lean

added theorem ContinuousMap.homotopic_const_iff

added def Path.toHomotopyConst