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"