Revision #2352 → #2735 · back to history
modifiedClosed interval is compact184c7c1f8f46
| Field | From #2352 | To #2735 |
|---|
| mathlib.decl | isCompact_Icc | CompactIccSpace.isCompact_Icc |
| provenance | ai | ai-moderated |
modifiedHausdorff distance is a metric on compact subsets0cedd3e46c10
| Field | From #2352 | To #2735 |
|---|
| mathlib.decl | NonemptyCompacts.instMetricSpace | Metric.NonemptyCompacts.instMetricSpace |
| provenance | ai | ai-moderated |
addedClosed set in a metric space92bbba43b5aa
addedMetric convergence agrees with topological convergence46f37cac4fe0
addedMetrizable implies paracompact Hausdorff and first-countable6d6302d0f8d8
addedBounded operator83ff55f18737
addedTriangle inequality for distance from a point to a setd6e9ec491089