Revision #3218 → #3739 · back to history
modifiedNagata–Smirnov metrization theoreme7a74f4930df
| Field | From #3218 | To #3739 |
|---|
| note | Grep for `NagataSmirnov` returns no matches; only Urysohn's metrization theorem is in Mathlib. | Loogle for `NagataSmirnov` returns no matches; only Urysohn's metrization theorem is in Mathlib. |
modifiedQuasi-isometric embeddingf81c9019484c
| Field | From #3218 | To #3739 |
|---|
| note | Grep for `QuasiIsometry` returns no matches in Mathlib. | Loogle for `QuasiIsometry` returns no matches in Mathlib. |
modifiedCayley graphdb1f8fee332c
| Field | From #3218 | To #3739 |
|---|
| mathlib.decl | — | SimpleGraph.mulCayley |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Cayley |
| note | No Cayley graph of a group with respect to a generating set is constructed in Mathlib. | `SimpleGraph.mulCayley s` (and `SimpleGraph.addCayley`) defines the Cayley graph of `M` with generating set `s`. |
| status | not_formalized | formalized |
modifiedWord metricc238cf6888f1
| Field | From #3218 | To #3739 |
|---|
| note | No `wordMetric` and no Cayley-graph metric construction in Mathlib. | Although `SimpleGraph.mulCayley` exists, no `wordMetric` combining Cayley graph with shortest-path distance is registered as a metric-space instance. |
modifiedLevenshtein distance6f2012bf2fef
| Field | From #3218 | To #3739 |
|---|
| note | No Levenshtein/edit-distance declaration exists in Mathlib; `decl_exists` and grep for `Levenshtein`/`EditDistance` return no matches. | No Levenshtein/edit-distance declaration exists in Mathlib; loogle for `Levenshtein`/`editDistance` returns no matches. |
addedRiemannian manifold as a metric space3cb1c2ca2d5a
addedUniform continuity (in the lead)ddb4104cf670
addedContraction has a unique fixed point3002d5613bda
addedCayley–Klein metric2685be75041b
addedSequential compactness equals compactness in metric spacesfeae36c7e49f