(def-constant quadratic%bound%at%point"lambda(f:[pp_0,pp_1], x:pp_0, forsome(a:rr, 0<=a and forall(y:pp_0,dist_1(f(x),f(y))<=dist_0(x,y)*(a+dist_0(x,y)))))"(theory metric-spaces-2-tuples))

(def-theorem quadratic-is-continuous"forall(f:[pp_0,pp_1], x:pp_0, quadratic%bound%at%point(f,x) implies continuous%at%point(f,x))"(proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (instantiate-existential ("min(1,eps/(1+a))")) (weaken (0)) (unfold-single-defined-constant (0) min) (case-split ("1<=eps/(1+a)")) simplify simplify (apply-macete-with-minor-premises fractional-expression-manipulation) simplify (apply-macete-with-minor-premises transitivity-of-<=) (instantiate-existential ("dist_0(x,y_$0)*(a+dist_0(x,y_$0))")) (apply-macete-with-minor-premises transitivity-of-<=) (instantiate-existential ("(eps/(1+a))*(a+1)")) (apply-macete-with-minor-premises monotone-product-lemma) (cut-with-single-formula"min(1,eps/(1+a))<=1 and min(1,eps/(1+a))<=eps/(1+a)") simplify (apply-macete-with-minor-premises minimum-2nd-arg) (apply-macete-with-minor-premises minimum-1st-arg) (apply-macete-with-minor-premises fractional-expression-manipulation) simplify )) (usages transportable-macete) (theory metric-spaces-2-tuples))

(def-theory-ensemble-instances metric-spaces force-under-quick-load (target-theories metric-spaces h-o-real-arithmetic h-o-real-arithmetic) (sorts (pp pp rr rr)) (constants (dist dist"lambda(x,y:rr, abs(x-y))""lambda(x,y:rr, abs(x-y))")) (permutations (1) (0 1) (1 2)))

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

(def-theorem square-is-quadratic"forall(x:rr,quadratic%bound%at%point(lambda(x:rr, x^2),x))"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (instantiate-existential ("2*abs(x)")) simplify (force-substitution"x^2-y_$1^2""(x-y_$1)*(x+y_$1)"(0)) (force-substitution"x+y_$1""(x+x)+(y_$1-x)"(0)) (apply-macete-with-minor-premises absolute-value-product) (apply-macete-with-minor-premises monotone-product-lemma) direct-and-antecedent-inference-strategy simplify simplify simplify unfold-defined-constants (weaken (0 1 2 3)) (prove-by-logic-and-simplification 3) simplify simplify )) (theory h-o-real-arithmetic))

(def-theorem multiplication-by-a-constant-is-quadratic"forall(a,x:rr,quadratic%bound%at%point(lambda(x:rr, a*x),x))"(proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (instantiate-existential ("abs(a)")) simplify (force-substitution"a*x-a*y_$1""a*(x-y_$1)"(0)) (apply-macete-with-minor-premises absolute-value-product) simplify simplify )) (theory h-o-real-arithmetic))

(def-theorem square-is-continuous"forall(x:rr, continuous%at%point(lambda(x:rr,x^2),x))"(proof ( (apply-macete-with-minor-premises tr%quadratic-is-continuous) (apply-macete-with-minor-premises square-is-quadratic) ) ) (theory h-o-real-arithmetic))

(def-theorem multiplication-by-a-constant-is-continuous"forall(a,x:rr,continuous%at%point(lambda(x:rr, a*x),x))"(proof ( (apply-macete-with-minor-premises tr%quadratic-is-continuous) (apply-macete-with-minor-premises multiplication-by-a-constant-is-quadratic) )) (theory h-o-real-arithmetic))

(def-theorem composition-of-continuous-is-continuous"forall(f:[pp,rr],g:[rr,rr],x:pp, continuous%at%point(f,x) and continuous%at%point(g,f(x)) implies continuous%at%point(g oo f,x))"(proof ( unfold-defined-constants beta-reduce-with-minor-premises direct-and-antecedent-inference-strategy (auto-instantiate-universal-antecedent"with(g:[rr,rr],x:pp,f:[pp,rr], forall(eps_$0:rr, 0<eps_$0 implies forsome(delta_$0:rr, 0<delta_$0 and forall(y_$0:rr, abs(f(x)-y_$0)<=delta_$0 implies abs(g(f(x))-g(y_$0))<=eps_$0))));") (instantiate-universal-antecedent"with(f:[pp,rr],x:pp, forall(eps:rr, 0<eps implies forsome(delta:rr, 0<delta and forall(y:pp, dist(x,y)<=delta implies abs(f(x)-f(y))<=eps))));"("delta_$0")) (instantiate-existential ("delta")) (backchain"with(eps_$0:rr,g:[rr,rr],delta_$0:rr,x:pp,f:[pp,rr], forall(y_$0:rr, abs(f(x)-y_$0)<=delta_$0 implies abs(g(f(x))-g(y_$0))<=eps_$0));") (backchain"with(delta_$0:rr,f:[pp,rr],delta:rr,x:pp, forall(y:pp, dist(x,y)<=delta implies abs(f(x)-f(y))<=delta_$0));") (cut-with-single-formula"abs(f(x)-f(y_$0))<=delta_$0") (instantiate-universal-antecedent"with(f:[pp,rr],x:pp, forall(eps:rr, 0<eps implies forsome(delta:rr, 0<delta and forall(y:pp, dist(x,y)<=delta implies abs(f(x)-f(y))<=eps))));"("1")) (simplify-antecedent"not(0<1);") (cut-with-single-formula"abs(f(x)-f(x))<=1") (backchain"with(f:[pp,rr],delta:rr,x:pp, forall(y:pp,dist(x,y)<=delta implies abs(f(x)-f(y))<=1));") simplify )) (theory metric-spaces))

(def-theorem sum-of-continuous-is-continuous"forall(f,g:[pp,rr], x:pp, continuous%at%point(f,x) and continuous%at%point(g,x) implies continuous%at%point(lambda(x:pp,f(x)+g(x)),x))"(proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("eps_$0/2")) (simplify-antecedent"with(p:prop, not(p))") (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("eps_$0/2")) (simplify-antecedent"with(p:prop, not(p))") (cut-with-single-formula"min(delta,delta_$0)<=delta and min(delta,delta_$0)<=delta_$0") (instantiate-existential ("min(delta,delta_$0)")) unfold-defined-constants (raise-conditional (0)) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises transitivity-of-<=) (instantiate-existential ("abs(f(x)-f(y_$1))+abs(g(x)-g(y_$1))")) (cut-with-single-formula"#(f(x)) and #(g(x)) and #(f(y_$1)) and #(g(y_$1))") unfold-defined-constants (weaken (1 2 3 4 5 6 7)) (prove-by-logic-and-simplification 3) simplify (instantiate-universal-antecedent"with(eps_$0:rr,f:[pp,rr],delta_$0:rr,x:pp, forall(y:pp, dist(x,y)<=delta_$0 implies abs(f(x)-f(y))<=eps_$0/2));"("y_$1")) (contrapose"with(p:prop, not(p))") simplify (instantiate-universal-antecedent"with(eps_$0:rr,g:[pp,rr],delta:rr,x:pp, forall(y:pp, dist(x,y)<=delta implies abs(g(x)-g(y))<=eps_$0/2));"("y_$1")) (contrapose"with(p:prop, not(p))") simplify simplify (cut-with-single-formula"abs(f(x)-f(y_$1))<=eps_$0/2 and abs(g(x)-g(y_$1))<=eps_$0/2") simplify direct-inference (backchain"with(eps_$0:rr,f:[pp,rr],delta_$0:rr,x:pp, forall(y:pp, dist(x,y)<=delta_$0 implies abs(f(x)-f(y))<=eps_$0/2));") simplify (backchain"with(eps_$0:rr,g:[pp,rr],delta:rr,x:pp, forall(y:pp, dist(x,y)<=delta implies abs(g(x)-g(y))<=eps_$0/2));") simplify (instantiate-universal-antecedent"with(eps_$0:rr,f:[pp,rr],delta_$0:rr,x:pp, forall(y:pp, dist(x,y)<=delta_$0 implies abs(f(x)-f(y))<=eps_$0/2));"("y_$1")) (instantiate-universal-antecedent"with(eps_$0:rr,g:[pp,rr],delta:rr,x:pp, forall(y:pp, dist(x,y)<=delta implies abs(g(x)-g(y))<=eps_$0/2));"("y_$1")) (apply-macete-with-minor-premises minimum-1st-arg) (apply-macete-with-minor-premises minimum-2nd-arg) ) ) (usages transportable-macete) (theory metric-spaces))

(def-schematic-macete abstraction-for-sum"with(a,b:rr, lambda(x:pp,a+b)=lambda(x:pp,lambda(x:pp,a)(x)+lambda(x:pp,b)(x)))"(theory metric-spaces) null)

(def-schematic-macete abstraction-for-square"with(a:rr, lambda(x:pp,a^2)=lambda(x:rr,x^2) oo lambda(x:pp,a))"(theory metric-spaces) null)

(def-schematic-macete abstraction-for-scalar-product"with(a,c:rr, lambda(x:pp,a * c)=lambda(x:rr,a * x) oo lambda(x:pp, c))"(theory metric-spaces) null)

(def-compound-macete abstraction (sound (series abstraction-for-sum abstraction-for-scalar-product abstraction-for-square) beta-reduce-unstoppably beta-reduce-unstoppably))

(def-compound-macete composite-continuity-macete (series (repeat abstraction sum-of-continuous-is-continuous composition-of-continuous-is-continuous square-is-continuous multiplication-by-a-constant-is-continuous) tr%unary-eta-reduction))

(def-theorem product-in-terms-of-squares-lemmaRemark: This entry is multiply defined. See: [1] [2]"forall(a,b:rr, a*b=1/2*((a+b)^2+[-1]*(a^2+b^2)))"(proof ( simplify )) (theory h-o-real-arithmetic))

(def-theorem continuous-at-point-defined"forall(f:[pp_0,pp_1], x:pp_0, continuous%at%point(f,x) implies #(f(x)))"(theory metric-spaces-2-tuples) (usages transportable-macete) (proof ( (unfold-single-defined-constant (0) continuous%at%point) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("1")) (simplify-antecedent"not(0<1);") (cut-with-single-formula"dist_1(f(x),f(x))<=1") (backchain"with(f:[pp_0,pp_1],delta:rr,x:pp_0, forall(y:pp_0, dist_0(x,y)<=delta implies dist_1(f(x),f(y))<=1));") (apply-macete-with-minor-premises tr%zero-self-distance) simplify ) ))

(def-theorem product-of-continous-is-continuous"forall(f,g:[pp,rr], x:pp, continuous%at%point(f,x) and continuous%at%point(g,x) implies continuous%at%point(lambda(x:pp, f(x)*g(x)),x))"(theory metric-spaces) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises product-in-terms-of-squares-lemma) direct-and-antecedent-inference-strategy (cut-with-single-formula"#(f(x)) and #(g(x))") (apply-macete-with-minor-premises composite-continuity-macete) simplify (apply-macete-with-minor-premises tr%continuous-at-point-defined) simplify )))

(def-theorem dist-uniformly-continuous"forall(y:pp,uniformly%continuous(lambda(x:pp,dist(x,y))))"(usages transportable-macete) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy auto-instantiate-existential (cut-with-single-formula"abs(dist(x_$1,y)-dist(y_$1,y))<=dist(x_$1,y_$1)") simplify (apply-macete-with-minor-premises dist-continuity-lemma) )) (theory metric-spaces))

(def-theorem constant-uniformly-continuous"forall(r:rr,uniformly%continuous(lambda(x:pp,r)))"(usages transportable-macete) (theory metric-spaces) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy auto-instantiate-existential (unfold-single-defined-constant (0) abs) simplify )))

(def-theorem constant-is-continuous"forall(r:rr,x:pp, continuous%at%point(lambda(x:pp,r),x))"(usages transportable-macete) (theory metric-spaces) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy auto-instantiate-existential (unfold-single-defined-constant (0) abs) simplify )))

(def-theorem identity-uniformly-continuous"uniformly%continuous(lambda(x:pp,x))"(usages transportable-macete) (theory metric-spaces) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy auto-instantiate-existential )))

(def-theorem composition-of-continuous-special-case"forall(f:[pp,pp],g:[pp,rr],x:pp, continuous%at%point(f,x) and continuous%at%point(g,f(x)) implies continuous%at%point(g oo f,x))"(proof ( unfold-defined-constants beta-reduce-with-minor-premises direct-and-antecedent-inference-strategy (auto-instantiate-universal-antecedent"with(p:prop,forall(eps:rr, 0<eps implies p))") (instantiate-universal-antecedent"with(p:prop,forall(eps:rr, 0<eps implies p))"("delta_$0")) (instantiate-existential ("delta")) (backchain"with(eps_$0:rr,g:[pp,rr],delta_$0:rr,x:pp,f:[pp,pp], forall(y_$0:pp, dist(f(x),y_$0)<=delta_$0 implies abs(g(f(x))-g(y_$0))<=eps_$0));") (backchain"with(delta_$0:rr,f:[pp,pp],delta:rr,x:pp, forall(y:pp, dist(x,y)<=delta implies dist(f(x),f(y))<=delta_$0));") (cut-with-single-formula"dist(f(x),f(y_$0))<=delta_$0") (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("1")) (simplify-antecedent"not(0<1);") (cut-with-single-formula"dist(f(x),f(x))<=1") (backchain"with(f:[pp,pp],delta:rr,x:pp, forall(y:pp,dist(x,y)<=delta implies dist(f(x),f(y))<=1));") simplify )) (usages transportable-macete) (theory metric-spaces))

(def-schematic-macete transportable-abstraction-for-sum"with(a,b:rr, lambda(x:ind_1,a+b)=lambda(x:ind_1,lambda(x:ind_1,a)(x)+lambda(x:ind_1,b)(x)))"(theory generic-theory-1) transportable null)

(def-schematic-macete transportable-abstraction-for-product"with(a,c:rr, lambda(x:ind_1,a * c)=lambda(x:ind_1,lambda(x:ind_1,a)(x) * lambda(x:ind_1, c)(x)))"(theory generic-theory-1) transportable null)

(def-compound-macete real-fn-abstraction (sound (series transportable-abstraction-for-sum transportable-abstraction-for-product) beta-reduce-unstoppably beta-reduce-unstoppably))

(def-compound-macete polynomial-continuity-macete (series (repeat (without-minor-premises exp-out) real-fn-abstraction tr%sum-of-continuous-is-continuous tr%product-of-continous-is-continuous tr%constant-is-continuous beta-reduce) tr%unary-eta-reduction))