(def-theory-ensemble-multiple metric-spaces 2)

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

(def-constant continuous%at%point 
    "lambda(f:[pp_0,pp_1],x:pp_0,forall(eps:rr,0<eps 
              implies 
              forsome(delta:rr,0<delta 
                    and forall(y:pp_0,dist_0(x,y)<=delta implies dist_1(f(x),f(y))<=eps))))"
    (theory metric-spaces-2-tuples))

(def-constant continuous 
    "lambda(f:[pp_0,pp_1],
          forall(v:sets[pp_1], open(v) implies open(inv_image(f,v))))"
    (theory metric-spaces-2-tuples))

(def-theory-ensemble-overloadings metric-spaces (2))

(def-theorem abstract-intermediate-value 
    "forall(f:[pp_0,pp_1],o:sets[pp_0],
continuous(f) and total_q(f,[pp_0,pp_1]) and connected(o) implies connected(image(f,o)))"
    (theory metric-spaces-2-tuples)
    (proof (unfold-defined-constants
	    (apply-macete-with-minor-premises direct-image-to-inverse-image-conversion-macete)
	    (prove-by-logic-and-simplification 3))))
	    

(def-theorem abstract-bolzano-weierstrass 
    "forall(f:[pp_0,pp_1],o:sets[pp_0],
continuous(f) and total_q(f,[pp_0,pp_1]) and compact(o) implies compact(image(f,o)))"
    (theory metric-spaces-2-tuples)
    (proof (unfold-defined-constants
	    (apply-macete-with-minor-premises covers-direct-image-to-inverse-image-conversion-macete)
	    (prove-by-logic-and-simplification 3))))

(def-theorem eps-delta-characterization-of-continuity 
    "forall(f:[pp_0,pp_1],total_q{f,[pp_0,pp_1]} 
                                      implies
                                    continuous(f) 
                                    iff
                                    forall(x:pp_0,continuous%at%point(f,x)))"
    (theory metric-spaces-2-tuples)
    (usages transportable-macete)
    (proof
      (
        unfold-defined-constants
        direct-inference
        direct-inference
        direct-inference
        (block (script-comment "node added by `direct-inference' at (0)")
	      (instantiate-universal-antecedent "with(p:prop,forall(v:sets[pp_1],p));"
					          (" open%ball(f(x),eps)"))
	      (block (script-comment "node added by `instantiate-universal-antecedent' at (0 0 0 0 0)")
		    (contrapose "with(p:prop,not(p));")
		    (apply-macete-with-minor-premises tr%open-balls-are-open))
	      (block (script-comment "node added by `instantiate-universal-antecedent' at (0 0 0 0 1)")
		    (incorporate-antecedent "with(f:sets[pp_0],open(f));")
		    unfold-defined-constants-repeatedly
		    simplify-insistently
		    direct-and-antecedent-inference-strategy
		    (instantiate-universal-antecedent "with(p:prop,forall(x_$2:pp_0,p implies p));"
						        ("x"))
		    (block (script-comment "node added by `instantiate-universal-antecedent' at (0 0 0)")
			  (contrapose "with(p:prop,not(p));")
			  (apply-macete-with-minor-premises tr%zero-self-distance))
		    (block (script-comment "node added by `instantiate-universal-antecedent' at (0 0 1 0 0)")
			  (instantiate-existential ("delta_$1"))
			  (auto-instantiate-universal-antecedent "with(eps:rr,f:[pp_0,pp_1],delta_$1:rr,x:pp_0,
    forall(x_$0:pp_0,
        dist_0(x,x_$0)<=delta_$1
          implies 
        dist_1(f(x),f(x_$0))<eps))")
			  simplify))
	      (unfold-single-defined-constant (0) open%ball_1))
        (block (script-comment "node added by `direct-inference' at (1)")
	      unfold-defined-constants-repeatedly
	      simplify-insistently
	      direct-and-antecedent-inference-strategy
	      (auto-instantiate-universal-antecedent "with(v:sets[pp_1],p:prop,forall(x:pp_1, x in v implies p))")
	      (instantiate-universal-antecedent "with(p:prop,forall(x:pp_0,forall(eps:rr,p)));"
					          ("x_$2"))
	      (auto-instantiate-universal-antecedent "with(p:prop, forall(eps:rr,0<eps implies p))")
	      (instantiate-existential ("delta_$0"))
	      (backchain-repeatedly ("with(v:sets[pp_1],delta:rr,x_$2:pp_0,f:[pp_0,pp_1],
    forall(x_$0:pp_1,
        dist_1(f(x_$2),x_$0)<=delta implies x_$0 in v))"))
	      (backchain "with(p:prop,forall(y_$0:pp_0,p implies p));"))
        )
      )
    )

(def-constant lipschitz%bound%on 
    "lambda(phi:[pp_0,pp_1],r:rr,s:sets[pp_0], 
          0<r and forall(x,y:pp_0, 
                              x in s and y in s 
                                implies  
                              dist_1(phi(x),phi(y)) <= r * dist_0(x,y)))"
    (theory metric-spaces-2-tuples))

(def-constant lipschitz%bound 
    "lambda(phi:[pp_0,pp_1],r:rr,
          lipschitz%bound%on(phi,r,sort_to_indic{pp_0}))"
    (theory  metric-spaces-2-tuples))

(def-theorem lipschitz-bound-is-total 
    "forall(f:[pp_0,pp_1],r:rr,
          lipschitz%bound(f,r) implies total_q{f,[pp_0,pp_1]})"
    (theory  metric-spaces-2-tuples)
    (usages transportable-macete)
    (proof 
      (
        unfold-defined-constants
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        simplify
        )))

(def-constant uniformly%continuous 
    "lambda(f:[pp_0,pp_1],
          forall(eps:rr, 
              0<eps 
                implies 
              forsome(delta:rr, 0<delta and
                  forall(x,y:pp_0, 
                      #(f(x)) and #(f(y)) and dist_0(x,y)<=delta 
                        implies 
                      dist_1(f(x),f(y))<=eps))))"
    (theory metric-spaces-2-tuples))

(def-theorem lipschitz-bound-is-uniformly-continuous 
    "forall(f:[pp_0,pp_1],r:rr, 
          lipschitz%bound(f,r) implies uniformly%continuous(f))"
    (theory metric-spaces-2-tuples)
    (usages transportable-macete)
    (proof
      (
        unfold-defined-constants
        (unfold-single-defined-constant (0) lipschitz%bound%on)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("eps/r"))
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        (apply-macete-with-minor-premises transitivity-of-<=)
        (instantiate-existential ("r*dist_0(x_$0,y_$0)"))
        (backchain 
            "with(r:rr,f:[pp_0,pp_1],forall(x_$0,y_$0:pp_0,
                  x_$0 in sort_to_indic{pp_0} and y_$0 in sort_to_indic{pp_0}
                    implies 
                  dist_1(f(x_$0),f(y_$0))<=r*dist_0(x_$0,y_$0)));")
        simplify
        (incorporate-antecedent 
          "with(r,eps:rr,y_$0,x_$0:pp_0,f:[pp_0,pp_1],
                #(f(x_$0)) and #(f(y_$0)) and dist_0(x_$0,y_$0)<=eps/r);")
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        simplify
        )))

(def-theorem total-uniformly-continuous-is-continuous 
    "forall(f:[pp_0,pp_1], 
          uniformly%continuous(f) and total_q{f,[pp_0,pp_1]}
            implies 
          forall(x:pp_0, continuous%at%point(f,x)))"
    (theory metric-spaces-2-tuples)
    (usages transportable-macete)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (auto-instantiate-universal-antecedent 
          "with(p:prop, forall(eps:rr, 0<eps implies p))")
        (instantiate-existential ("delta"))
        (backchain "with(p,q:prop, forall(x,y:pp_0, p implies q))")
        simplify
        )))

(def-theorem lipschitz-bound-is-continuous 
    "forall(f:[pp_0,pp_1],r:rr,x:pp_0, 
          lipschitz%bound(f,r) implies continuous%at%point(f,x))"
    (theory metric-spaces-2-tuples)
    (usages transportable-macete)
    (proof 
      (
        (apply-macete-with-minor-premises total-uniformly-continuous-is-continuous)
        (apply-macete-with-minor-premises lipschitz-bound-is-uniformly-continuous)
        (apply-macete-with-minor-premises lipschitz-bound-is-total)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("r"))
        )))