(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))