(def-theorem ptwise-continuity-is-closed-under-uniform-limits"forall(s:[zz,ms%bfun], x:pp_0, forsome(m:zz, forall(n:zz, m<=n implies continuous%at%point(s(n),x))) and #(lim(s)) implies continuous%at%point(lim(s),x))"(proof ( (unfold-single-defined-constant (0 1) continuous%at%point) direct-and-antecedent-inference-strategy (cut-with-single-formula"lim(s)=lim(s)") (incorporate-antecedent"with(s:[zz,ms%bfun],lim(s)=lim(s));") (apply-macete-with-minor-premises tr%characterization-of-limit) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("eps/3")) (simplify-antecedent"with(p:prop, not(p))") (instantiate-universal-antecedent"with(eps:rr,s:[zz,ms%bfun],n_$0:zz, forall(p_$0:zz, n_$0<=p_$0 implies dist(lim(s),s(p_$0))<=eps/3));"("max(n_$0,m)")) (contrapose"with(p:prop, not(p))") (apply-macete-with-minor-premises maximum-1st-arg) (instantiate-universal-antecedent"with(m:zz, p:prop, forall(n:zz, m<=n implies p))"("max(n_$0,m)")) (contrapose"with(p:prop, not(p))") (apply-macete-with-minor-premises maximum-2nd-arg) (beta-reduce-antecedent"with(f:[ms%bfun,pp_0,prop], a:ms%bfun,x:pp_0, f(a,x))") (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("eps/3")) (simplify-antecedent"with(p:prop, not(p))") (instantiate-existential ("delta_$0")) (instantiate-universal-antecedent"with(p:prop, forall(y:pp_0, p))"("y")) (cut-with-single-formula"dist_1(lim(s)(x),lim(s)(y))<=dist_1(lim(s)(x),s(max(n_$0,m))(x)) +dist_1(s(max(n_$0,m))(x),s(max(n_$0,m))(y))+dist_1(lim(s)(y),s(max(n_$0,m))(y)) and forall(x: pp_0, dist_1(lim(s)(x),s(max(n_$0,m))(x))<=dist(lim(s),s(max(n_$0,m))))") (antecedent-inference"with(p,q:prop, p and q)") (instantiate-universal-antecedent-multiply"with(p:prop,forall(x:pp_0,p));"(("x") ("y"))) simplify direct-and-antecedent-inference-strategy (weaken (1 2 4 5)) (cut-with-single-formula"total_q{dist_1,[pp_1,pp_1,rr]} and forall(x,y,z,u:pp_1, dist_1(x,u) <=dist_1(x,y)+dist_1(y,z)+dist_1(u,z))") (backchain"with(q,p:prop,q and p)") (weaken (0 2)) (apply-macete-with-minor-premises tr%bfun-values-defined-lemma) (weaken (0 2)) (weaken (0 1)) direct-and-antecedent-inference-strategy insistent-direct-inference (cut-with-single-formula"0<=dist_1(x_0,x_1)") (apply-macete-with-minor-premises tr%positivity-of-distance) (apply-macete-with-minor-premises tr%triangle-inequality-alternate-form) (instantiate-existential ("y")) simplify (apply-macete-with-minor-premises tr%triangle-inequality-alternate-form) (instantiate-existential ("z")) simplify (apply-macete-locally tr%symmetry-of-distance (0)" dist_1(z,u) ") simplify (apply-macete-with-minor-premises tr%bounded-bfun%dist) ) ) (theory pointed-ms-2-tuples))

(def-theorem continuity-is-closed-under-uniform-limits"forall(s:[zz,ms%bfun],x:pp_0, forsome(m:zz, forall(n:zz, m<=n implies total_q{s(n),[pp_0,pp_1]} and continuous(s(n)))) and #(lim(s)) implies continuous(lim(s)))"(usages transportable-macete) (theory pointed-ms-2-tuples) (proof ( (apply-macete-with-minor-premises eps-delta-characterization-of-continuity) (apply-macete-with-minor-premises ptwise-continuity-is-closed-under-uniform-limits) direct-and-antecedent-inference-strategy (instantiate-existential ("m")) (backchain"with(p:prop, m:zz, forall(n:zz, m<=n implies p))") insistent-direct-inference-strategy (apply-macete-with-minor-premises tr%bfun-values-defined-lemma) ) ))

(def-theorem ()"lambda(s:ms%bfun, continuous(s))(lambda(x:pp_0,a_0))"(proof ( (apply-macete-with-minor-premises eps-delta-characterization-of-continuity) (unfold-single-defined-constant (0) continuous%at%point) beta-reduce-with-minor-premises beta-reduce-repeatedly direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%zero-self-distance) simplify (instantiate-existential ("1")) simplify (apply-macete-with-minor-premises ms%bfun-defining-axiom_pointed-ms-2-tuples) insistent-direct-inference-strategy simplify (apply-macete-with-minor-premises tr%prec%sup-defined) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%non-empty-range) (instantiate-existential ("x_$0")) simplify-insistently (apply-macete-with-minor-premises tr%zero-self-distance) (instantiate-existential ("0")) (unfold-single-defined-constant (0) majorizes) simplify-insistently (apply-macete-with-minor-premises tr%zero-self-distance) simplify insistent-direct-inference-strategy (apply-macete-with-minor-premises tr%bfun-values-defined-lemma) ) ) (theory pointed-ms-2-tuples))

(def-atomic-sort continuous%bfun"lambda(s:ms%bfun, continuous(s))"(theory pointed-ms-2-tuples) (witness"lambda(x:pp_0,a_0)"))

(def-theory-ensemble-instances metric-spaces (target-theories pointed-ms-2-tuples) (multiples 1) (theory-interpretation-check using-simplification) (sorts (pp continuous%bfun)) (constants (dist"lambda(f,g: continuous%bfun, ms%bfun%dist(f,g))")) (special-renamings (ball cbfun%ball) (open%ball cbfun%open%ball) (lipschitz%bound cbfun%lipschitz%bound) (lipschitz%bound%on cbfun%lipschitz%bound%on) (complete cbfun%complete) (cauchy cbfun%cauchy) (lim cbfun%lim)))

(def-translation subspaces-to-function-subspace (source ms-subspace) (target pointed-ms-2-tuples) (fixed-theories h-o-real-arithmetic) (sort-pairs (aa continuous%bfun) (pp ms%bfun)) (constant-pairs (dist ms%bfun%dist)) (theory-interpretation-check using-simplification))

(def-theorem continuous%bfun%complete"complete_1 implies cbfun%complete"(proof ( (apply-macete-with-minor-premises tr%rev%completeness-extends) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%limit-definedness-extends) (apply-macete-with-minor-premises continuous%bfun-defining-axiom_pointed-ms-2-tuples) beta-reduce-repeatedly (apply-macete-with-minor-premises tr%rev%limit-definedness-extends) (apply-macete-with-minor-premises continuity-is-closed-under-uniform-limits) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(t:continuous%bfun,#(t))") (apply-macete-with-minor-premises tr%existence-of-limit) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))"("1")) (simplify-antecedent"with(p:prop,not(p))") (instantiate-existential ("n_$0")) insistent-direct-inference-strategy (cut-with-single-formula"forsome(f:ms%bfun,f=s(n))") (antecedent-inference"with(p:prop, forsome(f:ms%bfun,p))") (backchain-backwards"with(f,g: ms%bfun, f=g)") (apply-macete-with-minor-premises tr%bfun-values-defined-lemma) (instantiate-existential ("s(n)")) (instantiate-universal-antecedent"with(p:prop, forall(n:zz,p))"("n")) (instantiate-universal-antecedent"with(p:prop, forall(n:zz,p))"("n")) (apply-macete-with-minor-premises continuous%bfun-in-quasi-sort_pointed-ms-2-tuples) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%limit-definedness-extends) (apply-macete-with-minor-premises continuous%bfun-defining-axiom_pointed-ms-2-tuples) beta-reduce-repeatedly (apply-macete-with-minor-premises continuous%bfun-in-quasi-sort_pointed-ms-2-tuples) (apply-macete-with-minor-premises tr%rev%limit-definedness-extends) (apply-macete-with-minor-premises tr%bfun-completeness) )) (theory pointed-ms-2-tuples))