Mathlib v3 is deprecated. Go to Mathlib v4

Theorem path.homotopic.hcomp

Modification history

2021-11-15 21:01

src/topology/homotopy/path.lean

feat(topology/homotopy/fundamental_groupoid): The functor from `Top` to `Groupoid` (#10195) …

Added path.homotopic.hcomp View on Github →