Revision #1099 → #2539 · back to history
modifiedUniversal property of completion380d5cdcb783
| Field | From #1099 | To #2539 |
|---|
| mathlib.decl | Completion.extension_unique | UniformSpace.Completion.extension_unique |
| provenance | ai | ai-moderated |
modifiedDistance on Cauchy sequences is a pseudometric40d9c63216ab
| Field | From #1099 | To #2539 |
|---|
| mathlib.decl | Completion.instPseudoMetricSpace | UniformSpace.Completion.instMetricSpace |
| provenance | ai | ai-moderated |
modifiedEmbedding into completion defines an isometry onto dense subspaced5ac04c39b7a
| Field | From #1099 | To #2539 |
|---|
| mathlib.decl | Completion.coe_isometry | UniformSpace.Completion.coe_isometry |
| provenance | ai | ai-moderated |
modifiedCompleteness is a metric property, not topological9de5290fa986
| Field | From #1099 | To #2539 |
|---|
| mathlib.decl | IsCompletelyMetrizableSpace | TopologicalSpace.IsCompletelyMetrizableSpace |
| provenance | ai | ai-moderated |
modifiedCompletely metrizable space8c5646262f9f
| Field | From #1099 | To #2539 |
|---|
| mathlib.decl | IsCompletelyMetrizableSpace | TopologicalSpace.IsCompletelyMetrizableSpace |
| provenance | ai | ai-moderated |