Revision #1633 → #1808 · back to history
modifiedBasic topological propertiesd5a03cfa23c6
| Field | From #1633 | To #1808 |
|---|
| note | Dimension as a topological invariant is partially captured by `smallInductiveDimension`, but the general list of invariants is not a decl. | Dimension as a topological invariant is partially captured by `smallInductiveDimension`, but the general list of invariants is not a single decl. |
modifiedSeven Bridges of Königsbergcce32a36c57f
| Field | From #1633 | To #1808 |
|---|
| note | Mathlib has the `IsEulerian` infrastructure but the actual Königsberg theorem (`Konigsberg.not_isEulerian`) lives in Archive, not Mathlib/. | Mathlib has the `IsEulerian` infrastructure but the actual Königsberg theorem lives in Archive, not in Mathlib/. |
modifiedHairy ball theorem170ab9453491
| Field | From #1633 | To #1808 |
|---|
| note | The hairy ball theorem appears only as an unproven title in docs/1000.yaml with no Mathlib decl. | The hairy ball theorem has no corresponding Mathlib decl. |
modifiedEuler's polyhedron formula6353a9792ce3
| Field | From #1633 | To #1808 |
|---|
| note | The polyhedron formula V−E+F=2 appears only as an unproven title in docs/100.yaml with no decl. | The polyhedron formula V−E+F=2 has no Mathlib decl. |
addedHausdorff space3ace8dd6c853
addedTopological continuity agrees with ε-δ continuity on ℝ2f54f9cf277a
modifiedOpen set in a metric space9f85e8d89a29
| Field | From #1633 | To #1808 |
|---|
| note | `Metric.isOpen_iff` characterizes open sets as those containing a ball around each point. | `Metric.isOpen_iff` characterizes open sets in a metric space as those containing a ball around each point. |
addedHomotopy groups3e780b7f3cd4
modifiedUniformization theoremb312b1f31cd5
| Field | From #1633 | To #1808 |
|---|
| note | The uniformization theorem appears only as an unproven title in docs/1000.yaml with no decl. | The uniformization theorem has no Mathlib decl. |
modifiedConfiguration space3b6816b256b6
| Field | From #1633 | To #1808 |
|---|
| note | Mathlib has no robotics configuration-space manifold definition (only an unrelated symbolic-dynamics usage of the term). | Mathlib has no robotics configuration-space manifold definition. |
addedEulerian path in modular fiber arte85a03d64048