1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/ftc/WeakIVT".
19 (* $Id: WeakIVT.v,v 1.9 2004/04/23 10:01:01 lcf Exp $ *)
21 (*#* printing ** %\ensuremath\times% #×# *)
31 (*#* *IVT for Partial Functions
33 In general, we cannot prove the classically valid Intermediate Value
34 Theorem for arbitrary partial functions, which states that in any
35 interval [[a,b]], for any value [z] between [f(a)] and [f(b)]
36 there exists $x\in[a,b]$#x∈[a,b]# such that [f(x) [=] z].
38 However, as is usually the case, there are some good aproximation results. We
46 inline cic:/CoRN/ftc/WeakIVT/a.var.
48 inline cic:/CoRN/ftc/WeakIVT/b.var.
50 inline cic:/CoRN/ftc/WeakIVT/Hab.var.
54 inline cic:/CoRN/ftc/WeakIVT/I.con.
58 inline cic:/CoRN/ftc/WeakIVT/F.var.
60 inline cic:/CoRN/ftc/WeakIVT/contF.var.
64 %\begin{convention}% Let [a, b : IR] and [Hab : a [<=] b] and denote by [I]
65 the interval [[a,b]]. Let [F] be a continuous function on [I].
68 We begin by proving that, if [f(a) [<] f(b)], then for every [y] in
69 [[f(a),f(b)]] there is an $x\in[a,b]$#x∈[a,b]# such that [f(x)] is close
73 inline cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_lft.con.
83 inline cic:/CoRN/ftc/WeakIVT/a.var.
85 inline cic:/CoRN/ftc/WeakIVT/b.var.
87 inline cic:/CoRN/ftc/WeakIVT/Hab.var.
91 inline cic:/CoRN/ftc/WeakIVT/I.con.
95 inline cic:/CoRN/ftc/WeakIVT/F.var.
97 inline cic:/CoRN/ftc/WeakIVT/contF.var.
100 If [f(b) [<] f(a)], a similar result holds:
103 inline cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_rht.con.
115 We will now assume that [a [<] b] and that [F] is not only
116 continuous, but also strictly increasing in [I]. Under
117 these assumptions, we can build two sequences of values which
118 converge to [x0] such that [f(x0) [=] z].
121 inline cic:/CoRN/ftc/WeakIVT/a.var.
123 inline cic:/CoRN/ftc/WeakIVT/b.var.
125 inline cic:/CoRN/ftc/WeakIVT/Hab'.var.
127 inline cic:/CoRN/ftc/WeakIVT/Hab.var.
131 inline cic:/CoRN/ftc/WeakIVT/I.con.
135 inline cic:/CoRN/ftc/WeakIVT/F.var.
137 inline cic:/CoRN/ftc/WeakIVT/contF.var.
141 inline cic:/CoRN/ftc/WeakIVT/incF.con.
147 inline cic:/CoRN/ftc/WeakIVT/incrF.var.
153 inline cic:/CoRN/ftc/WeakIVT/Ha.con.
155 inline cic:/CoRN/ftc/WeakIVT/Hb.con.
157 inline cic:/CoRN/ftc/WeakIVT/HFab'.con.
163 inline cic:/CoRN/ftc/WeakIVT/z.var.
165 inline cic:/CoRN/ftc/WeakIVT/Haz.var.
167 inline cic:/CoRN/ftc/WeakIVT/Hzb.var.
171 (*#* Given any two points [x [<] y] in [[a,b]] such that [x [<=] z [<=] y],
172 we can find [x' [<] y'] such that $|x'-y'|=\frac23|x-y|$#|x'-y'|=2/3|x-y|#
173 and [x' [<=] z [<=] y'].
176 inline cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con.
181 We now iterate this construction.
184 inline cic:/CoRN/ftc/WeakIVT/IVT_aux_seq_type.ind.
186 inline cic:/CoRN/ftc/WeakIVT/IVT_iter.con.
188 inline cic:/CoRN/ftc/WeakIVT/IVT_seq.con.
191 We now define the sequences built from this iteration, starting with [a] and [b].
194 inline cic:/CoRN/ftc/WeakIVT/a_seq.con.
196 inline cic:/CoRN/ftc/WeakIVT/b_seq.con.
198 inline cic:/CoRN/ftc/WeakIVT/a_seq_I.con.
200 inline cic:/CoRN/ftc/WeakIVT/b_seq_I.con.
202 inline cic:/CoRN/ftc/WeakIVT/a_seq_less_b_seq.con.
204 inline cic:/CoRN/ftc/WeakIVT/a_seq_leEq_z.con.
206 inline cic:/CoRN/ftc/WeakIVT/z_leEq_b_seq.con.
208 inline cic:/CoRN/ftc/WeakIVT/a_seq_mon.con.
210 inline cic:/CoRN/ftc/WeakIVT/b_seq_mon.con.
212 inline cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist_n.con.
214 inline cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist.con.
216 inline cic:/CoRN/ftc/WeakIVT/a_seq_Cauchy.con.
218 inline cic:/CoRN/ftc/WeakIVT/b_seq_Cauchy.con.
220 inline cic:/CoRN/ftc/WeakIVT/xa.con.
222 inline cic:/CoRN/ftc/WeakIVT/xb.con.
224 inline cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_lim.con.
226 inline cic:/CoRN/ftc/WeakIVT/xa_in_interval.con.
228 inline cic:/CoRN/ftc/WeakIVT/IVT_I.con.