The path-class universal cover dependency map
This map shows the container's direct articles. Nested containers are collapsed and clickable; dependency edges are rolled up from their leaves. in mathlib1Upstreamed into Mathlib.fully proved12Proved, and every prerequisite is fully proved too.
graph LR
n0("Small nullhomotopy neighborhoods form a basis"):::fully_proved
n1["Semilocally simply-connected spaces"]:::fully_proved
n2("The sets U[γ] form the universal-cover basis"):::fully_proved
n3("The endpoint map is a covering"):::fully_proved
n4["The path-class cover is path-connected"]:::fully_proved
n5["The path-class universal-cover space"]:::fully_proved
n6("The path-class cover is simply-connected"):::fully_proved
n7["External chapter: The fundamental group<br/><small>6 items · 1 in mathlib · 5 fully proved</small>"]:::boundary
n7 -. 2 .-> n6
n0 -.-> n2
n1 -->|2| n7
n1 --> n0
n1 --> n5
n2 -.-> n7
n2 -.-> n3
n2 -.-> n4
n3 -.-> n7
n3 -.-> n6
n4 -.-> n7
n4 -.-> n6
n5 --> n7
n5 --> n2
n5 --> n3
n5 --> n4
n5 --> n6
click n0 "../../../../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#nullhomotopic-open-basis" "Small nullhomotopy neighborhoods form a basis — 1 item · 1 fully proved"
click n1 "../../../../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#semilocally-simply-connected" "Semilocally simply-connected spaces — 1 item · 1 fully proved"
click n2 "../../../../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-basis" "The sets U[γ] form the universal-cover basis — 1 item · 1 fully proved"
click n3 "../../../../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-is-covering" "The endpoint map is a covering — 1 item · 1 fully proved"
click n4 "../../../../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-path-connected" "The path-class cover is path-connected — 1 item · 1 fully proved"
click n5 "../../../../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-path-space" "The path-class universal-cover space — 1 item · 1 fully proved"
click n6 "../../../../roadmap/fundamental-group/covering-spaces/universal-cover/index.html#universal-cover-simply-connected" "The path-class cover is simply-connected — 1 item · 1 fully proved"
click n7 "../../../chapters/fundamental-group.html" "The fundamental group — 6 items · 1 in mathlib · 5 fully proved"