```
(def-theorem uniform-continuity-is-closed-under-uniform-limits
"forall(s:[zz,ms%bfun],x:pp_0,
forsome(m:zz,
forall(n:zz,
m<=n
implies
uniformly%continuous(s(n))))
and
#(lim(s))
implies
uniformly%continuous(lim(s)))"
(usages transportable-macete)
(theory pointed-ms-2-tuples)
(proof
(

(force-substitution "uniformly%continuous(s(n))" "total_q{s(n),[pp_0,pp_1]} and uniformly%continuous(s(n))" (0))
(unfold-single-defined-constant (0 1) uniformly%continuous)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "lim(s)=lim(s)")
(incorporate-antecedent "with(s:[zz,ms%bfun],lim(s)=lim(s));")
(apply-macete-with-minor-premises tr%characterization-of-limit)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr,0<eps implies p))" ("eps/3"))
(simplify-antecedent "with(p:prop, not(p))")
(instantiate-universal-antecedent "with(eps:rr,s:[zz,ms%bfun],n_\$0:zz,
forall(p_\$0:zz,
n_\$0<=p_\$0 implies dist(lim(s),s(p_\$0))<=eps/3));" ("max(n_\$0,m)"))
(contrapose "with(p:prop, not(p))")
(apply-macete-with-minor-premises maximum-1st-arg)
(instantiate-universal-antecedent "with(m:zz, p:prop,  forall(n:zz,  m<=n implies p))" ("max(n_\$0,m)"))
(contrapose "with(p:prop, not(p))")
(apply-macete-with-minor-premises maximum-2nd-arg)
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr,  0<eps implies p))" ("eps/3"))
(simplify-antecedent "with(p:prop, not(p))")
(instantiate-existential ("delta_\$0"))
(instantiate-universal-antecedent "with(p:prop, forall(x,y:pp_0, p))" ("x" "y"))
(contrapose "with(x:pp_0,m,n_\$0:zz,s:[zz,ms%bfun],
not(#(s(max(n_\$0,m))(x))));")
(contrapose "with(y:pp_0,m,n_\$0:zz,s:[zz,ms%bfun],
not(#(s(max(n_\$0,m))(y))));")
(cut-with-single-formula "dist_1(lim(s)(x),lim(s)(y))<=dist_1(lim(s)(x),s(max(n_\$0,m))(x))
+dist_1(s(max(n_\$0,m))(x),s(max(n_\$0,m))(y))+dist_1(lim(s)(y),s(max(n_\$0,m))(y)) and forall(x:
pp_0, dist_1(lim(s)(x),s(max(n_\$0,m))(x))<=dist(lim(s),s(max(n_\$0,m))))")
(antecedent-inference "with(p,q:prop, p and q)")
(instantiate-universal-antecedent-multiply
"with(r:rr,forall(x:pp_0,r<=r));"
(("x") ("y")))
simplify
direct-and-antecedent-inference-strategy
(weaken (0 2 4 6))
(cut-with-single-formula "total_q{dist_1,[pp_1,pp_1,rr]} and forall(x,y,z,u:pp_1, dist_1(x,u)
<=dist_1(x,y)+dist_1(y,z)+dist_1(u,z))")
(backchain "with(q,p:prop,q and p)")
(weaken (0 1 2))
direct-and-antecedent-inference-strategy
insistent-direct-inference
(cut-with-single-formula "0<=dist_1(x_0,x_1)")
(apply-macete-with-minor-premises tr%positivity-of-distance)
(apply-macete-with-minor-premises tr%triangle-inequality-alternate-form)
(instantiate-existential ("y"))
simplify
(apply-macete-with-minor-premises tr%triangle-inequality-alternate-form)
(instantiate-existential ("z"))
simplify
(apply-macete-locally tr%symmetry-of-distance (0) " dist_1(z,u) ")
simplify
(apply-macete-with-minor-premises tr%bounded-bfun%dist)
direct-and-antecedent-inference-strategy
insistent-direct-inference
(apply-macete-with-minor-premises tr%bfun-values-defined-lemma)
)
))
```

```(def-theorem ()
"lambda(s:ms%bfun, uniformly%continuous(s))(lambda(x:pp_0,a_0))"
(proof
(
(unfold-single-defined-constant (0) uniformly%continuous)
beta-reduce-with-minor-premises
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%zero-self-distance)
simplify
(instantiate-existential ("1"))
simplify
(apply-macete-with-minor-premises ms%bfun-defining-axiom_pointed-ms-2-tuples)
insistent-direct-inference-strategy
simplify
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%non-empty-range)
(instantiate-existential ("x_\$0"))
simplify-insistently
(apply-macete-with-minor-premises tr%zero-self-distance)
(instantiate-existential ("0"))
(unfold-single-defined-constant (0) majorizes)
simplify-insistently
(apply-macete-with-minor-premises tr%zero-self-distance)
simplify
)
)
(theory pointed-ms-2-tuples))
```

```
(def-atomic-sort unif%continuous%bfun
"lambda(s:ms%bfun, uniformly%continuous(s))"
(theory pointed-ms-2-tuples)
(witness "lambda(x:pp_0,a_0)"))
```

```(def-theorem ()
"forall(x,y,z:unif%continuous%bfun, dist(x,z)<=dist(y,z)+dist(x,y))"
(theory pointed-ms-2-tuples)
(proof
(
(apply-macete-with-minor-premises tr%triangle-inequality-for-distance)
)))
```

```(def-theory-ensemble-instances
metric-spaces
(target-theories pointed-ms-2-tuples)
(multiples 1)
(theory-interpretation-check using-simplification)
(sorts (pp unif%continuous%bfun))
(constants (dist "lambda(f,g: unif%continuous%bfun, ms%bfun%dist(f,g))"))
(special-renamings
(ball ucbfun%ball)
(open%ball ucbfun%open%ball)
(lipschitz%bound ucbfun%lipschitz%bound)
(lipschitz%bound%on ucbfun%lipschitz%bound%on)
(complete ucbfun%complete)
(cauchy ucbfun%cauchy)
(lim ucbfun%lim)))
```

```
(def-translation subspaces-to-uc-function-subspace
(source ms-subspace)
(target pointed-ms-2-tuples)
(fixed-theories h-o-real-arithmetic)
(sort-pairs (aa unif%continuous%bfun) (pp ms%bfun))
(constant-pairs (dist ms%bfun%dist))
(theory-interpretation-check using-simplification))
```

```
(def-theorem uniformly%continuous%bfun%complete
"complete_1 implies ucbfun%complete"

(proof
(
(apply-macete-with-minor-premises tr%rev%completeness-extends)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%limit-definedness-extends)
(apply-macete-with-minor-premises unif%continuous%bfun-defining-axiom_pointed-ms-2-tuples)
beta-reduce-repeatedly
(apply-macete-with-minor-premises tr%rev%limit-definedness-extends)
(apply-macete-with-minor-premises uniform-continuity-is-closed-under-uniform-limits)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(t:unif%continuous%bfun,#(t))")
(apply-macete-with-minor-premises tr%existence-of-limit)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("1"))
(simplify-antecedent "with(p:prop,not(p))")
(instantiate-existential ("n_\$0"))
insistent-direct-inference-strategy
(cut-with-single-formula "forsome(f:ms%bfun,f=s(n))")
(antecedent-inference "with(p:prop, forsome(f:ms%bfun,p))")
(backchain-backwards "with(f,g: ms%bfun, f=g)")
(apply-macete-with-minor-premises unif%continuous%bfun-in-quasi-sort_pointed-ms-2-tuples)
(instantiate-existential ("s(n)"))
(instantiate-universal-antecedent "with(p:prop, forall(n:zz,p))" ("n"))
(instantiate-universal-antecedent "with(p:prop, forall(n:zz,p))" ("n"))
(apply-macete-with-minor-premises tr%limit-definedness-extends)
(apply-macete-with-minor-premises tr%bfun-completeness)
))
(usages transportable-macete)
(theory pointed-ms-2-tuples))
```