```
(def-theorem lipschitz%bound-translation-inversion
"forall(phi:[uu,uu],s:sets[uu],y:uu,c:rr,
lipschitz%bound%on(phi,c,s)
implies
lipschitz%bound%on(lambda(x:uu,[-1]*phi(x)+y),c,s))"
lemma
(theory normed-linear-spaces)
(proof
(
unfold-defined-constants
(force-substitution "norm(phi(x)-phi(y))" "norm([-1]*(phi(x)-phi(y)))" (0))
simplify
(apply-macete-with-minor-premises norm-scalar-multiplication)
(apply-macete-with-minor-premises absolute-value-non-positive)
simplify
)))
```

```
(def-theorem open-mapping-lemma
"forall(phi:[uu,uu],b:uu,r,c:rr,
complete and lipschitz%bound%on(phi,c,ball(b,r))  and c<1 and 0<=r
implies
open%ball(lambda(z:uu,phi(z) + z)(b),(1-c)*r)
subseteq
image(lambda(z:uu,phi(z) + z),ball(b,r)))"
lemma
(theory normed-linear-spaces)

(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "#(phi(b))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(unfold-single-defined-constant (0) open%ball) simplify-insistently
direct-and-antecedent-inference-strategy
(force-substitution "x_\$0=x+phi(x)" "lambda(x:uu, x_\$0+[-1]*phi(x))(x)=x" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises tr%restricted-fixed-point-theorem)
(instantiate-existential ("c"))
(block
(script-comment "`instantiate-existential' at (0 2)")
(apply-macete-with-minor-premises %vector-plus-commutativity)
(apply-macete-with-minor-premises lipschitz%bound-translation-inversion)
)
simplify
)
simplify
)
(block
(script-comment "`cut-with-single-formula' at (1)")
(incorporate-antecedent
"with(f:sets[uu],c:rr,phi:[uu,uu],
lipschitz%bound%on(phi,c,f));"
)
unfold-defined-constants simplify-insistently direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(x_\$0,y_\$0:uu,p));" ("b" "b"))
(contrapose "with(p:prop,not(p));")
simplify
)
)))
```

```
(def-theorem image-contained-in-range
"forall(s:sets[ind_1],f:[ind_1,ind_2], image(f,s) subseteq ran(f))"
lemma
(theory generic-theory-2)
(usages transportable-macete)
(proof (simplify-insistently
direct-and-antecedent-inference-strategy
auto-instantiate-existential)))
```

```
(def-theorem lipschitz%bound%on%subsets
"forall(phi:[pp_0,pp_1],s,s_1:sets[pp_0],r:rr,s subseteq s_1 and
lipschitz%bound%on(phi,r,s_1) implies lipschitz%bound%on(phi,r,s))"
lemma
(theory metric-spaces-2-tuples)
(proof
(

(unfold-single-defined-constant (0 1) lipschitz%bound%on)
(prove-by-logic-and-simplification 3)
))
(usages transportable-macete))
```

```
(def-theorem open-mapping
"forall(phi:[uu,uu],b:uu,c:rr,
complete and lipschitz%bound%on(phi,c,dom{phi})  and c<1
implies
(open(dom{phi}) implies open(ran{lambda(z:uu,phi(z)+z)})))"
(theory normed-linear-spaces)
(proof
(
(unfold-single-defined-constant (0 1) open)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(x_\$2:uu,phi:[uu,uu],x_\$2 in ran{lambda(z:uu,phi(z)+z)});")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(phi:[uu,uu],
forall(x_\$2:uu,
x_\$2 in dom{phi}
implies
forsome(delta_\$0:rr,
0<delta_\$0 and ball(x_\$2,delta_\$0) subseteq dom{phi})));" ("x"))
(contrapose "with(x:uu,phi:[uu,uu],not(x in dom{phi}));")
simplify
(instantiate-existential ("(1-c)*delta_\$1/2"))
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(apply-macete-with-minor-premises tr%subseteq-transitivity)
(instantiate-existential ("image(lambda(z:uu,phi(z)+z),ball(x,delta_\$1))"))
(apply-macete-with-minor-premises tr%subseteq-transitivity)
(instantiate-existential ("open%ball(lambda(x:uu,phi(x)+x)(x),(1-c)*delta_\$1)"))
simplify