Convex sets have trivial fundamental group: 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.

in mathlib2Upstreamed into Mathlib.

graph LR n0("Simply connected spaces have unique path-homotopy classes"):::mathlib n1("Convex sets have trivial fundamental group"):::mathlib n0 -.-> n1 click n0 "../../../../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" class n1 focus click n1 "../../../../roadmap/fundamental-group/basic-constructions/index.html#convex-trivial-fundamental-group" "Convex sets have trivial fundamental group — 1 item · 1 in mathlib"