| changeset 51523 | 97b5e8a1291c |
| parent 51521 | 36fa825e0ea7 |
| 51522:bd568f4bf446 | 51523:97b5e8a1291c |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Metric Spaces *} |
6 header {* Metric Spaces *} |
7 |
7 |
8 theory Metric_Spaces |
8 theory Metric_Spaces |
9 imports RealDef Topological_Spaces |
9 imports Real Topological_Spaces |
10 begin |
10 begin |
11 |
11 |
12 |
12 |
13 subsection {* Metric spaces *} |
13 subsection {* Metric spaces *} |
14 |
14 |