Mayer–Vietoris sequences 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 mathlib2Upstreamed into Mathlib.fully proved13Proved, and every prerequisite is fully proved too.
graph LR
n0("Augmented binary-cover chains form a short exact sequence"):::fully_proved
n1["The binary-cover Mayer–Vietoris chain complex"]:::fully_proved
n2("Binary-cover chains form a short exact sequence"):::fully_proved
n3("The binary-cover Mayer–Vietoris sequence"):::fully_proved
n4("The reduced binary-cover Mayer–Vietoris sequence"):::fully_proved
n5["Small augmented chains include by a chain-homotopy equivalence"]:::fully_proved
n6["External chapter: Homology<br/><small>9 items · 2 in mathlib · 7 fully proved</small>"]:::boundary
n6 --> n0
n6 -->|2| n1
n6 --> n3
n6 -. 2 .-> n3
n6 --> n4
n6 -.-> n4
n6 -->|2| n5
n0 --> n4
n1 --> n0
n1 --> n2
n2 -.-> n0
n2 --> n3
n3 --> n6
n4 --> n6
n5 --> n0
n5 -.-> n4
click n0 "../../../../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#augmented-binary-cover-chain-short-exact-sequence" "Augmented binary-cover chains form a short exact sequence — 1 item · 1 fully proved"
click n1 "../../../../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#binary-cover-chain-complex" "The binary-cover Mayer–Vietoris chain complex — 1 item · 1 fully proved"
click n2 "../../../../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#binary-cover-chain-short-exact-sequence" "Binary-cover chains form a short exact sequence — 1 item · 1 fully proved"
click n3 "../../../../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#binary-cover-mayer-vietoris-sequence" "The binary-cover Mayer–Vietoris sequence — 1 item · 1 fully proved"
click n4 "../../../../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#reduced-binary-cover-mayer-vietoris-sequence" "The reduced binary-cover Mayer–Vietoris sequence — 1 item · 1 fully proved"
click n5 "../../../../roadmap/homology/computations-and-applications/mayer-vietoris/index.html#small-augmented-chain-inclusion-homotopy-equivalence" "Small augmented chains include by a chain-homotopy equivalence — 1 item · 1 fully proved"
click n6 "../../../chapters/homology.html" "Homology — 9 items · 2 in mathlib · 7 fully proved"