(def-theory-ensemble-instances metric-spaces force-under-quick-load (permutations (0 1)) (sorts (pp pp pp)) (constants (dist dist dist)) (target-theories metric-spaces metric-spaces))

(def-theory-ensemble-instances metric-spaces force-under-quick-load (permutations (0)) (sorts (pp bfun)) (constants (dist bfun%dist)) (target-theories mappings-into-a-pointed-metric-space) (special-renamings (ball bfun%ball) (complete bfun%complete) (lipschitz%bound%on bfun%lipschitz%bound%on) (lipschitz%bound bfun%lipschitz%bound)))

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

(def-theorem bfun-values-defined-lemma"forall(x:ind_1,g:bfun, #(g(x)))"(usages rewrite transportable-macete) (proof ( (instantiate-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space ("g")) simplify simplify ) ) (theory mappings-into-a-pointed-metric-space))

(def-theorem bfun-ball-membership-lemma"forall(f:[ind_1,pp],g:bfun, r:rr, f in ball(g,r) iff forall(x:ind_1, f(x) in ball(g(x),r)))"(proof ( direct-inference (force-substitution"f in ball(g,r) ""forsome(h:bfun, h=f and h in ball(g,r))"(0)) (apply-macete-with-minor-premises ball-membership-condition) (apply-macete-with-minor-premises tr%ball-membership-condition) (force-substitution"bfun%dist(g,h)<=r""forall(x:ind_1,dist(g(x),h(x))<=r)"(0)) direct-and-antecedent-inference-strategy (backchain-backwards"with(f:[ind_1,pp],h:bfun,h=f);") simplify (instantiate-existential ("f")) (apply-macete-with-minor-premises bfun-defining-axiom_mappings-into-a-pointed-metric-space) insistent-direct-inference insistent-direct-inference (apply-macete-with-minor-premises tr%prec%sup-defined) direct-and-antecedent-inference-strategy (weaken (1)) (apply-macete-with-minor-premises tr%non-empty-range) (instantiate-existential ("x")) (unfold-single-defined-constant (0) rad%dist) simplify (weaken (0 1)) (unfold-single-defined-constant (0) rad%dist) (apply-macete-with-minor-premises tr%prec%majorizes%characterization) beta-reduce-repeatedly (instantiate-existential ("r+sup(ran{rad%dist oo g})")) (apply-macete-with-minor-premises triangle-inequality-alternate-form) (instantiate-existential ("g(n_$0)")) (cut-with-single-formula"dist(a_0,g(n_$0))<=sup(ran{rad%dist oo g})") simplify (apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup) direct-and-antecedent-inference-strategy (instantiate-existential ("dist(g(n_$0),a_0)")) (unfold-single-defined-constant (0) rad%dist) simplify (instantiate-existential ("n_$0")) simplify simplify (weaken (0 1 2 3)) (cut-with-single-formula"#(g,bfun)") (incorporate-antecedent"with(g:bfun,#(g,bfun));") (apply-macete-with-minor-premises bfun-defining-axiom_mappings-into-a-pointed-metric-space) direct-and-antecedent-inference-strategy (weaken (0 1)) (weaken (0)) (weaken (0)) direct-and-antecedent-inference-strategy (cut-with-single-formula"dist(g(x),h(x))<=bfun%dist(g,h)") simplify (apply-macete-with-minor-premises bounded-bfun%dist) (unfold-single-defined-constant (0) bfun%dist) (apply-macete-with-minor-premises tr%lub-property-of-prec%sup) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%prec%majorizes%characterization) beta-reduce-repeatedly direct-and-antecedent-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) beta-reduce-repeatedly (instantiate-existential ("x")) (apply-macete-with-minor-premises tr%prec%majorizes%characterization) beta-reduce-repeatedly (instantiate-existential ("r")) direct-and-antecedent-inference-strategy (instantiate-existential ("f")) (backchain-backwards"with(f:[ind_1,pp],h:bfun,h=f);") ) ) (theory mappings-into-a-pointed-metric-space))

(def-theorem bfun-ball-closure"forall(f:bfun,r:rr, s:[zz,bfun],0<r and forall(n:zz, #(s(n)) implies s(n) in ball(f,r)) and forall(x:ind_1, #(lim(lambda(n:zz, s(n)(x))))) implies lambda(x:ind_1, lim(lambda(n:zz, s(n)(x)))) in ball(f,r))"(proof ( (apply-macete-with-minor-premises bfun-ball-membership-lemma) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises closed-balls-are-closed) direct-and-antecedent-inference-strategy simplify-insistently direct-and-antecedent-inference-strategy (backchain"with(x:ind_1,x_$1:zz,s:[zz,bfun],x_$0:pp,x_$0=s(x_$1)(x));") (backchain"with(r:rr,f:bfun,s:[zz,bfun], forall(n:zz, #(s(n)) implies forall(x:ind_1,s(n)(x) in ball(f(x),r))));") (instantiate-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space ("f")) simplify simplify ) ) (theory mappings-into-a-pointed-metric-space))

(def-theorem bfun-ball-closure-corollary"forall(f:bfun,r:rr, s:[zz,bfun],0<r and forsome(m:zz, forall(n:zz, m<=n implies s(n) in ball(f,r))) and forall(x:ind_1, #(lim(lambda(n:zz, s(n)(x))))) implies lambda(x:ind_1, lim(lambda(n:zz, s(n)(x)))) in ball(f,r))"(proof ( direct-and-antecedent-inference-strategy (force-substitution"lim(lambda(n:zz,s(n)(x)))""lim(lambda(n:zz,lambda(k:zz, if(m<=k,s(k),?bfun))(n)(x)))"(0)) (apply-macete-with-minor-premises bfun-ball-closure) beta-reduce-repeatedly direct-and-antecedent-inference-strategy simplify (cut-with-single-formula"lim(lambda(n:zz,if(m<=n, s(n), ?bfun)(x)))=lim(lambda(n:zz,s(n)(x)))") (weaken (0)) (apply-macete-with-minor-premises limit-depends-on-tail) direct-and-antecedent-inference-strategy (instantiate-existential ("m")) simplify (weaken (3)) (cut-with-single-formula"total_q{s(p_$1),[ind_1,pp]}") (instantiate-universal-antecedent"with(s:[zz,bfun],r:rr,f:bfun,m:zz,forall(n:zz,m<=n implies s(n) in ball(f,r)));"("p_$1")) (weaken ( 1 2)) (instantiate-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space ("s(p_$1)")) beta-reduce-repeatedly ) ) (theory mappings-into-a-pointed-metric-space))

(def-theorem uniform-cauchy-implies-ptwise-cauchy"forall(s:[zz,bfun], cauchy(s) implies forall(x:ind_1, cauchy(lambda(n:zz, s(n)(x)))))"(proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (auto-instantiate-universal-antecedent"with(s:[zz,bfun], forall(eps:rr, 0<eps implies forsome(p:zz, forall(q:zz,p<q implies bfun%dist(s(p),s(q))<=eps))));") (instantiate-existential ("p")) (apply-macete-with-minor-premises transitivity-of-<=) (instantiate-existential ("bfun%dist(s(p),s(q_$0))")) (apply-macete-with-minor-premises bounded-bfun%dist) (instantiate-universal-antecedent"with(eps_$0:rr,s:[zz,bfun],p:zz, forall(q:zz,p<q implies bfun%dist(s(p),s(q))<=eps_$0));"("q_$0")) (instantiate-universal-antecedent"with(eps_$0:rr,s:[zz,bfun],p:zz, forall(q:zz,p<q implies bfun%dist(s(p),s(q))<=eps_$0));"("q_$0")) (backchain"with(eps_$0:rr,s:[zz,bfun],p:zz, forall(q:zz,p<q implies bfun%dist(s(p),s(q))<=eps_$0));") direct-inference direct-inference ) ) (theory mappings-into-a-pointed-metric-space))

(def-theorem cauchy-ptwise-converge-implies-uniform-convergence"forall(s:[zz,bfun],cauchy(s) and forall(x:ind_1, #(lim(lambda(n:zz, s(n)(x))))) implies lim(s)=lambda(x:ind_1,(lim(lambda(n:zz, s(n)(x))))))"(proof ( (apply-macete-with-minor-premises tr%cauchy-double-index-characterization) (force-substitution"bfun%dist(s(p),s(q))<=eps""s(q) in ball(s(p),eps)"(0)) (block (script-comment"node added by `force-substitution' at (0)") direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(h:bfun, h = lambda(x:ind_1,lim(lambda(n:zz,s(n)(x)))))") (block (script-comment"node added by `cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(h:bfun,p));") (backchain-backwards"with(f:[ind_1,pp],h:bfun,h=f);") (apply-macete-with-minor-premises tr%characterization-of-limit) (force-substitution"bfun%dist(h,s(p))<=eps""h in ball(s(p),eps)"(0)) (block (script-comment"node added by `force-substitution' at (0)") direct-and-antecedent-inference-strategy (auto-instantiate-universal-antecedent"with(p:prop, forall(eps:rr, 0<eps implies p))") (instantiate-existential ("n")) (backchain"with(f:[ind_1,pp],h:bfun,h=f);") (apply-macete-with-minor-premises bfun-ball-closure-corollary) (block (script-comment"node added by `apply-macete-with-minor-premises' at (0)") direct-and-antecedent-inference-strategy (instantiate-existential ("n")) (backchain"with(p:prop,forall(p,q:zz,with(p:prop,p)));") simplify) (instantiate-universal-antecedent"with(p:prop,forall(p,q:zz,with(p:prop,p)));"("p""p"))) (block (script-comment"node added by `force-substitution' at (1)") (apply-macete-with-minor-premises tr%ball-membership-condition) direct-inference (apply-macete-with-minor-premises tr%symmetry-of-distance))) (block (script-comment"node added by `cut-with-single-formula' at (1)") (instantiate-universal-antecedent"with(p:prop,forall(eps:rr,p));"("1")) (simplify-antecedent"with(p:prop,not(p));") (block (script-comment"node added by `instantiate-universal-antecedent' at (0 0 1 0)") (cut-with-single-formula"lambda(x:ind_1,lim(lambda(n:zz,s(n)(x)))) in ball(s(n),1)") (block (script-comment"node added by `cut-with-single-formula' at (0)") (cut-with-single-formula"#(lambda(x:ind_1,lim(lambda(n:zz,s(n)(x)))),bfun)") (instantiate-existential ("lambda(x:ind_1,lim(lambda(n:zz,s(n)(x))))"))) (block (script-comment"node added by `cut-with-single-formula' at (1)") (apply-macete-with-minor-premises bfun-ball-membership-lemma) direct-and-antecedent-inference-strategy beta-reduce-repeatedly (force-substitution"lim(lambda(n:zz,s(n)(x)))""lim(lambda(k:zz,if(n<=k,s(k)(x),?pp)))"(0)) (block (script-comment"node added by `force-substitution' at (0)") (apply-macete-with-minor-premises closed-balls-are-closed) (block (script-comment"node added by `apply-macete-with-minor-premises' at (0)") direct-and-antecedent-inference-strategy (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (0)") simplify-insistently direct-and-antecedent-inference-strategy (cut-with-single-formula"forall(p,q:zz,n<=p and n<=q implies s(q)(x) in ball(s(p)(x),1))") (block (script-comment"node added by `cut-with-single-formula' at (0)") (force-substitution"x_$0""s(x_$1)(x)"(0)) (backchain"with(f:sets[pp], forall(p,q:zz, with(p:pp,p:prop, with(p:prop,p and p) implies with(p:pp,p in f))));") simplify) (block (script-comment"node added by `cut-with-single-formula' at (1)") (weaken (3 1 0)) (incorporate-antecedent"with(p:prop,p);") (apply-macete-with-minor-premises tr%ball-membership-condition) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises transitivity-of-<=) (block (script-comment"node added by `apply-macete-with-minor-premises' at (0)") (instantiate-existential ("bfun%dist(s(p),s(q))")) (block (script-comment"node added by `instantiate-existential' at (0 0)") (apply-macete-with-minor-premises bounded-bfun%dist) (instantiate-universal-antecedent"with(p:prop,forall(p,q:zz,with(p:prop,p)));"("p""q")) (instantiate-universal-antecedent"with(p:prop,forall(p,q:zz,with(p:prop,p)));"("p""q"))) simplify direct-and-antecedent-inference-strategy) (apply-macete-with-minor-premises bfun-values-defined-lemma))) (block (script-comment"node added by `direct-and-antecedent-inference-strategy' at (1)") (force-substitution"#(lim(lambda(k:zz,if(n<=k, s(k)(x), ?pp))))""lim(lambda(k:zz,if(n<=k, s(k)(x), ?pp)))=lim(lambda(n:zz,s(n)(x)))"(0)) (block (script-comment"node added by `force-substitution' at (0)") (weaken ("with(a,b:sets[pp], a subseteq b)")) (apply-macete-with-minor-premises limit-depends-on-tail) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (instantiate-existential ("n")) simplify (apply-macete-with-minor-premises bfun-values-defined-lemma) (instantiate-universal-antecedent"with(p:prop,forall(p,q:zz,with(p:prop,p)));"("n""p_$0")) (simplify-antecedent"with(p:prop,not(p));")) direct-and-antecedent-inference-strategy)) (block (script-comment"node added by `apply-macete-with-minor-premises' at (1)") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises bfun-values-defined-lemma) (instantiate-universal-antecedent"with(p:prop,forall(p,q:zz,with(p:prop,p)));"("n""n")) (simplify-antecedent"with(p:prop,not(p));"))) simplify)))) (apply-macete-with-minor-premises tr%ball-membership-condition) ) ) (theory mappings-into-a-pointed-metric-space))

(def-theorem bfun-completeness"complete implies bfun%complete"(proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (force-substitution"#(lim(s))""lim(s)=lambda(x:ind_1,lim(lambda(n:zz, s(n)(x))))"(0)) (apply-macete-with-minor-premises cauchy-ptwise-converge-implies-uniform-convergence) direct-and-antecedent-inference-strategy (backchain"forall(s:[zz,pp],cauchy(s) implies #(lim(s)));") (apply-macete-with-minor-premises uniform-cauchy-implies-ptwise-cauchy) direct-and-antecedent-inference-strategy ) ) (usages transportable-macete) (theory mappings-into-a-pointed-metric-space))