(def-constant continuous%at%point%rr
"lambda(f:[rr,rr], x:rr ,forall(eps:rr,0<eps
implies
forsome(delta:rr,0<delta
and forall(y:rr,abs(x-y)<=delta implies abs(f(x)-f(y))<=eps))))"
(theory h-o-real-arithmetic))
(def-theorem sup-property-of-continuity
Remark: This entry is multiply defined. See: [1] [2]
"forall(f:[rr,rr],x,a:rr,s:sets[rr],
continuous%at%point%rr(f,sup(s))
and
forall(x:rr,x in s implies f(x)<=a)
implies
f(sup(s))<=a)"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally continuous%at%point%rr)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "#(sup(s)) and #(f(sup(s)))")
(move-to-sibling 1)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(r:rr,with(f:[[rr,rr],rr,prop],f)(with(f:[rr,rr],f),r));")
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,
forall(eps:rr,0<eps implies forsome(delta:rr,p)));"
("1"))
(simplify-antecedent "with(p:prop,not(p));")
(instantiate-universal-antecedent "with(delta,r:rr,forall(y:rr,r<=delta implies r<=1));"
("sup(s)"))
(contrapose "with(p:prop,not(p));")
(unfold-single-defined-constant-globally abs)
simplify
(incorporate-antecedent "with(r:rr,with(f:[[rr,rr],rr,prop],f)(with(f:[rr,rr],f),r));")
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,
forall(eps:rr,0<eps implies forsome(delta:rr,p)));")
(instantiate-existential ("(f(sup(s))-a)/2"))
simplify
(cut-with-single-formula "forsome(x:rr, x in s and sup(s)-delta_$0<x)")
(instantiate-existential ("x"))
(apply-macete-with-minor-premises absolute-value-non-negative)
simplify
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(instantiate-existential ("x"))
simplify
(cut-with-single-formula "f(x)<=a")
(move-to-sibling 1)
simplify
(apply-macete-with-minor-premises absolute-value-non-negative)
simplify
(apply-macete-with-minor-premises sup-minus-epsilon-corollary)
direct-and-antecedent-inference-strategy
)))
(def-theorem lower-semicontinuity-of-continuous
"forall(f:[rr,rr],x,a:rr,
continuous%at%point%rr(f,x)
and
f(x)<a
implies
forsome(x_0:rr, x<x_0 and forall(y:rr,x<=y and y<=x_0 implies f(y)<a)))"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant-globally continuous%at%point%rr)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(eps:rr,p));"
("(a-f(x))/2"))
(simplify-antecedent "with(p:prop,not(p));")
(instantiate-existential ("x+delta_$0"))
simplify
(instantiate-universal-antecedent "with(p:prop,forall(y_$0:rr,p));" ("y_$0"))
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises absolute-value-non-positive)
simplify
(cut-with-single-formula "f(x)<=f(y_$0) or f(y_$0)<=f(x)")
(move-to-sibling 1)
simplify
(incorporate-antecedent "with(r:rr,r<=r);")
(antecedent-inference "with(p:prop,p or p);")
(apply-macete-with-minor-premises absolute-value-non-positive)
simplify
(apply-macete-with-minor-premises absolute-value-non-negative)
simplify
)))
(def-theorem intermediate-value-theorem
"forall(f:[rr,rr], a,b:rr,
a<=b
and
forall(x:rr, a<=x and x<=b implies continuous%at%point%rr(f,x))
and
f(a)<0
and
0<f(b)
implies
forsome(z:rr, a<=z and z<=b and f(z)=0))"
(theory fixed-interval-theory)
(proof
(
direct-and-antecedent-inference-strategy
(contrapose "with(r:rr,0<r);")
(cut-with-single-formula "forall(x:rr, a<=x and x<=b implies f(x)<=0)")
(instantiate-universal-antecedent "with(r:rr,p:prop,forall(x:rr,p and p implies r<=0));"
("b"))
(simplify-antecedent "with(p:prop,not(p));")
simplify
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forall(x:rr, a<=x implies x in indic{z:rr,z<=b implies f(z)<=0})")
(incorporate-antecedent "with(f:sets[rr],a:rr,forall(x:rr,a<=x implies x in f));")
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,a:rr,forall(x:rr,a<=x implies (p implies p)));")
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%induction-in-cpos)
direct-and-antecedent-inference-strategy
(instantiate-existential ("a"))
simplify-insistently
simplify-insistently
(apply-macete-with-minor-premises sup-property-of-continuity)
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,forall(x:rr,p implies p));")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-inference
(instantiate-existential ("a"))
simplify
(antecedent-inference "with(p:prop,p and p and p);")
(incorporate-antecedent "with(f,t_$0:sets[rr],t_$0 subseteq f);")
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,t_$0:sets[rr],
forall(x_$1:rr,x_$1 in t_$0 implies (p implies p)));")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("sup(t_$0)"))
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-inference
(instantiate-existential ("x_$1"))
simplify
(case-split ("b<=y_$1"))
(instantiate-existential ("z_$0"))
simplify-insistently
simplify
simplify
(cut-with-single-formula "f(y_$1)<=0 and not(f(y_$1)=0)")
(move-to-sibling 1)
direct-and-antecedent-inference-strategy
(antecedent-inference "with(p:prop,p and p and p and p);")
(incorporate-antecedent "with(y_$1:rr,f:[rr,rr],b:rr,
y_$1 in indic{z:rr, z<=b implies f(z)<=0});")
simplify-insistently
(backchain "with(p:prop,forall(z:rr,p or p or p));")
simplify
(cut-with-single-formula "y_$1<b and f(y_$1)<0")
(move-to-sibling 1)
simplify
(weaken (2 1))
(cut-with-single-formula
"forsome(x_0:rr, y_$1<x_0 and forall(y:rr,y_$1<=y and y<=x_0
implies
f(y)<0))")
(antecedent-inference-strategy (0))
simplify-insistently
(cut-with-single-formula
"forsome(w:rr, y_$1<w and w<=x_0 and w<=z_$0 and w<=b)")
(instantiate-existential ("w"))
(instantiate-universal-antecedent
"with(r:rr,p:prop,forall(y:rr,p and p implies r<0));"
("w"))
(simplify-antecedent "with(p:prop,not(p));")
simplify
simplify
simplify
(instantiate-existential ("min(x_0,min(z_$0,b))"))
unfold-defined-constants
(case-split ("z_$0<=b"))
simplify
(case-split ("x_0<=z_$0"))
simplify
simplify
simplify
(case-split ("x_0<=b"))
simplify
simplify
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("min(z_$0,b)"))
(apply-macete-with-minor-premises minimum-2nd-arg)
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises transitivity-of-<=)
(instantiate-existential ("min(z_$0,b)"))
(apply-macete-with-minor-premises minimum-2nd-arg)
(apply-macete-with-minor-premises minimum-2nd-arg)
(apply-macete-with-minor-premises lower-semicontinuity-of-continuous)
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,forall(x:rr,p implies p));")
simplify
)))