```(def-language language-for-ms-subspace
(embedded-languages metric-spaces-language)
(sorts (aa pp)))

```

```
(def-theory ms-subspace
(component-theories metric-spaces)
(language language-for-ms-subspace))
```

```(def-theorem ()
"forall(x,y,z:aa,dist(x,z)<=dist(y,z)+dist(x,y))"
lemma
(theory ms-subspace)
(proof
(
(apply-macete-with-minor-premises triangle-inequality-for-distance)
)))
```

```(def-theory-ensemble-instances
metric-spaces
(target-theories ms-subspace ms-subspace)
(multiples 1 2)
(theory-interpretation-check using-simplification)
(sorts (pp aa aa))
(constants (dist "lambda(x,y:aa, dist(x,y))" "lambda(x,y:aa, dist(x,y))"))
(special-renamings
(ball sub%ball)
(open%ball sub%open%ball)
(lipschitz%bound sub%lipschitz%bound)
(lipschitz%bound%on sub%lipschitz%bound%on)
(complete sub%complete)
(cauchy sub%cauchy)
(lim sub%lim)))
```

```
(def-theorem cauchy-extends
"forall(s:[zz,aa],cauchy(s) iff sub%cauchy(s))"
(proof (unfold-defined-constants))
(usages transportable-macete)
(theory ms-subspace))
```

```
(def-constant subspace%closed
"forall(s:[zz,aa], #(lim(s)) implies #(lim(s),aa))"
(theory ms-subspace))
```

```
(def-theorem limit-definedness-extends
"forall(s:[zz,aa],subspace%closed implies lim(s) == sub%lim(s))"
reverse
(usages transportable-macete)
(proof
((unfold-single-defined-constant (0) subspace%closed)
insistent-direct-inference-strategy
(antecedent-inference "with(s:[zz,aa],#(lim(s)) or #(sub%lim(s)));")
(force-substitution "lim(s)=sub%lim(s)" "sub%lim(s)=lim(s)" (0))
(cut-with-single-formula "forsome(x:aa, lim(s)=x)")
(antecedent-inference "with(s:[zz,aa],forsome(x:aa,lim(s)=x));")
(backchain "with(x:aa,s:[zz,aa],lim(s)=x);")
(apply-macete-with-minor-premises tr%characterization-of-limit)
beta-reduce-repeatedly
(backchain-backwards "with(x:aa,s:[zz,aa],lim(s)=x);")
(cut-with-single-formula "lim(s)=lim(s)")
(incorporate-antecedent "with(s:[zz,aa],lim(s)=lim(s));")
(apply-macete-with-minor-premises characterization-of-limit)
(instantiate-existential ("lim(s)"))
simplify
(apply-macete-with-minor-premises characterization-of-limit)
(cut-with-single-formula "sub%lim(s)=sub%lim(s)")
(incorporate-antecedent "with(s:[zz,aa],sub%lim(s)=sub%lim(s));")
(apply-macete-with-minor-premises tr%characterization-of-limit)
beta-reduce-repeatedly))
(theory ms-subspace))
```

```
(def-theorem completeness-extends
"complete implies subspace%closed iff sub%complete"
reverse
(proof
(
(unfold-single-defined-constant (0) complete)
(unfold-single-defined-constant (0) sub%complete)
(force-substitution "sub%cauchy(s)" "cauchy(s)" (0))
direct-and-antecedent-inference-strategy
(force-substitution "sub%lim(s)" "lim(s)" (0))
(backchain "forall(s:[zz,pp],cauchy(s) implies #(lim(s)));")
(apply-macete-with-minor-premises limit-definedness-extends)
(unfold-single-defined-constant (0) subspace%closed)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "forall(s:[zz,aa],cauchy(s) implies #(sub%lim(s)));" ("s"))
(contrapose "with(s:[zz,aa],not(cauchy(s)));")
(apply-macete-with-minor-premises convergent-implies-cauchy)
(cut-with-single-formula "forsome(x:aa, lim(s)=x)")
(antecedent-inference "with(s:[zz,aa],forsome(x:aa,lim(s)=x));")
(instantiate-existential ("sub%lim(s)"))
(apply-macete-with-minor-premises characterization-of-limit)
(cut-with-single-formula "sub%lim(s)=sub%lim(s)")
(incorporate-antecedent "with(s:[zz,aa],sub%lim(s)=sub%lim(s));")
(apply-macete-with-minor-premises tr%characterization-of-limit)
beta-reduce-repeatedly
(apply-macete-with-minor-premises cauchy-extends)
))

(usages transportable-macete)
(theory ms-subspace))
```

```
(def-constant subspace%dense
"forall(x:pp, forsome(s:[zz,aa], lim(s)=x))"
(theory ms-subspace))
```