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 include "CoRN_notation.ma".
21 (* $Id: WeakIVT.v,v 1.9 2004/04/23 10:01:01 lcf Exp $ *)
23 (*#* printing ** %\ensuremath\times% #×# *)
29 include "ftc/Continuity.ma".
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".