(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))