```(def-theory-ensemble-instances metric-spaces
(target-multiple 2)
(multiples 1))
```

```(def-theory-ensemble-overloadings metric-spaces (1))
```

```
(def-theorem lim-preservation
"forall(f:[pp_0,pp_1],x:pp_0,s:[zz,pp_0],continuous%at%point(f,lim(s)) implies
lim(f oo s)=f(lim(s)))"
(theory metric-spaces-2-tuples)
(usages transportable-macete)
reverse
(proof
(
(force-substitution "continuous%at%point(f,lim(s))" "lim(s)=lim(s) and continuous%at%point(f,lim(s))" (0))
(unfold-single-defined-constant (0) continuous%at%point)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%characterization-of-limit)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "#(lim(s))")
(incorporate-antecedent "with(s:[zz,pp_0],lim(s)=lim(s));")
(apply-macete-with-minor-premises tr%characterization-of-limit)
direct-and-antecedent-inference-strategy
(auto-instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies forsome(delta:rr, 0<delta and p)))")
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("delta"))
(instantiate-existential ("n_\$0"))
simplify-insistently
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies forsome(delta:rr, 0<delta and p)))" ("1"))
(simplify-antecedent "with(p:prop, not(p))")
(instantiate-universal-antecedent "with(f:[pp_0,pp_1],delta:rr,s:[zz,pp_0],
forall(y:pp_0,
dist_0(lim(s),y)<=delta
implies
dist_1(f(lim(s)),f(y))<=1));" ("lim(s)"))
(contrapose "with(p:prop, not(p))")
(apply-macete-with-minor-premises tr%zero-self-distance)
simplify
simplify
)))
```

```
(def-theorem lim-preservation-global
"forall(f:[pp_0,pp_1],total_q{f,[pp_0,pp_1]} and continuous(f) implies forall(s:[zz,pp_0],#(lim(s)) implies
lim(f oo s)=f(lim(s))))"
(theory metric-spaces-2-tuples)
(proof

(
(apply-macete-with-minor-premises eps-delta-characterization-of-continuity)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises lim-preservation)

)
))
```

```(def-script use-minimum-values 3
(
(cut-with-single-formula (% "forsome(~a:rr, 0<~a and ~a <=~a and ~a<=~a)"
\$1 \$1 \$1 \$2 \$1 \$3))
(label-node with-cut)
(move-to-sibling 1)
(instantiate-existential ((% "min(~a,~a)" \$2 \$3)))
(unfold-single-defined-constant (0) min)
(case-split ((% "~a<=~a" \$2 \$3)))
simplify
simplify
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises minimum-2nd-arg)
(jump-to-node with-cut)))

```

```
(def-theorem splicing-continuous-functions-lemma-1
"forall(f,g:[pp_0,pp_1], s:sets[pp_0],x:pp_0,
continuous%at%point(f,x) and
continuous%at%point(g,x) and
f(x)=g(x)
implies
continuous%at%point(lambda(z:pp_0,if(z in s, f(z),g(z))),x))"
(theory metric-spaces-2-tuples)
(usages transportable-macete)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy

(instantiate-universal-antecedent "with(p:prop,forall(eps:rr,p));" ("eps_\$0"))
(instantiate-universal-antecedent "with(p:prop,forall(eps:rr,p));" ("eps_\$0"))
(use-minimum-values "delta_1" "delta_\$0" "delta")
(instantiate-existential ("delta_1"))
(case-split ("x in s" "y_\$0 in s"))
simplify
simplify
(backchain "with(p:pp_1,p=p);")
simplify
simplify
(backchain-backwards "with(p:pp_1,p=p);")
simplify
simplify
)))
```

```
(def-theorem splicing-continuous-functions-lemma-2
"forall(f,g:[pp_0,pp_1],x:pp_0,
continuous%at%point(f,x)
and
forsome(r:rr,
0<r
and
forall(z:pp_0,z in open%ball(x,r) implies f(z)=g(z)))
implies
continuous%at%point(g,x))"
(theory metric-spaces-2-tuples)
(usages transportable-macete)
(proof
(

(unfold-single-defined-constant-globally continuous%at%point)
(apply-macete-with-minor-premises tr%open-ball-membership-condition)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(eps:rr,p));" ("eps"))
(use-minimum-values  "delta_1" "r/2" "delta")
(instantiate-existential ("delta_1"))
(backchain-backwards "with(p:pp_1,r:rr,forall(z:pp_0,r<r implies p=p));")
(backchain-backwards "with(p:pp_1,r:rr,forall(z:pp_0,r<r implies p=p));")
direct-and-antecedent-inference-strategy
simplify
(apply-macete-with-minor-premises tr%zero-self-distance)
simplify)))
```