(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
        (apply-macete-with-minor-premises tr%ball-subset-larger-radius-open-ball)
        simplify
        (apply-macete-with-minor-premises open-mapping-lemma)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%lipschitz%bound%on%subsets)
        auto-instantiate-existential
        simplify
        (apply-macete-with-minor-premises tr%image-contained-in-range)
        )))