Simply connected spaces have unique path-homotopy classes: local context

Project map · Chapter map · Full theorem DAG · Open textbook statement

This local map shows one dependency hop in either direction. The highlighted item is the current focus. What the colours mean

in mathlib3Upstreamed into Mathlib.

graph LR n0("Path homotopy is an equivalence relation"):::mathlib n1("Simply connected spaces have unique path-homotopy classes"):::mathlib n2("Convex sets have trivial fundamental group"):::mathlib n0 --> n1 n1 -.-> n2 click n0 "../../../../roadmap/fundamental-group/basic-constructions/index.html#path-homotopy-equivalence" "Path homotopy is an equivalence relation — 1 item · 1 in mathlib" class n1 focus click n1 "../../../../roadmap/fundamental-group/basic-constructions/index.html#simply-connected-unique-path-classes" "Simply connected spaces have unique path-homotopy classes — 1 item · 1 in mathlib" click n2 "../../../../roadmap/fundamental-group/basic-constructions/index.html#convex-trivial-fundamental-group" "Convex sets have trivial fundamental group — 1 item · 1 in mathlib"