```(def-language metric-spaces-language
(embedded-languages h-o-real-arithmetic)
(base-types pp)
(constants
(dist (pp pp rr))))

```

```
(def-theory metric-spaces
(component-theories h-o-real-arithmetic)
(language metric-spaces-language)
(axioms
(positivity-of-distance
"forall(x,y:pp, 0<=dist(x,y))" transportable-macete)
(point-separation-for-distance
"forall(x,y:pp, x=y iff dist(x,y)=0)" transportable-macete)
(symmetry-of-distance
"forall(x,y:pp, dist(x,y) = dist(y,x))" transportable-macete)
(triangle-inequality-for-distance
"forall(x,y,z:pp, dist(x,z)<=dist(x,y)+dist(y,z))" transportable-macete)))
```

```(def-theory-ensemble metric-spaces (fixed-theories h-o-real-arithmetic))
```

```
(def-constant ball
"lambda(x:pp,r:rr,indic{y:pp, dist(x,y)<=r})"
(theory metric-spaces)
(usages transportable-macete))
```

```
(def-constant open%ball
"lambda(x:pp,r:rr,indic{y:pp, dist(x,y)<r})"
(theory metric-spaces)
(usages transportable-macete))
```

```
(def-constant open
"lambda(o:sets[pp],forall(x:pp, x in o implies
forsome(delta:rr,0<delta and ball(x,delta) subseteq o)))"
(theory metric-spaces)
(usages transportable-macete))
```

```
(def-constant connected
Remark: This entry is multiply defined. See:  [1] [2]
"lambda(x:sets[pp],forall(a,b:sets[pp],open(a) and open(b) and empty_indic_q((a inters b) inters x) and x subseteq a union b implies (x subseteq a or x subseteq b)))"
(theory metric-spaces)
(usages transportable-macete))
```

```
(def-constant compact
"lambda(a:sets[pp], forall(f:[zz,sets[pp]],forall(i:zz,#(f(i)) implies open(f(i))) and countable%cover(f,a) implies finite%cover(f,a)))"
(theory metric-spaces)
(usages transportable-macete))
```