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/reals/IVT".
19 (* $Id: IVT.v,v 1.5 2004/04/23 10:01:04 lcf Exp $ *)
26 Section Nested_Intervals.
29 (*#* * Intermediate Value Theorem
33 %\begin{convention}% Let [a,b:nat->IR] be sequences such that:
36 - [forall (i:nat), (a i) [<] (b i)];
37 - for every positive real number [eps], there is an [i] such that [(b i) [<] (a i) [+]eps].
42 inline cic:/CoRN/reals/IVT/a.var.
44 inline cic:/CoRN/reals/IVT/b.var.
46 inline cic:/CoRN/reals/IVT/a_mon.var.
48 inline cic:/CoRN/reals/IVT/b_mon.var.
50 inline cic:/CoRN/reals/IVT/a_b.var.
52 inline cic:/CoRN/reals/IVT/b_a.var.
54 inline cic:/CoRN/reals/IVT/a_mon'.con.
56 inline cic:/CoRN/reals/IVT/b_mon'.con.
58 inline cic:/CoRN/reals/IVT/a_b'.con.
60 inline cic:/CoRN/reals/IVT/intervals_cauchy.con.
64 inline cic:/CoRN/reals/IVT/a'.con.
68 inline cic:/CoRN/reals/IVT/Cnested_intervals_limit.con.
70 (*#* %\begin{convention}% Let [f] be a continuous real function.
74 inline cic:/CoRN/reals/IVT/f.var.
76 inline cic:/CoRN/reals/IVT/f_contin.var.
78 inline cic:/CoRN/reals/IVT/f_contin_pos.con.
80 inline cic:/CoRN/reals/IVT/f_contin_neg.con.
82 (*#* Assume also that [forall i, f (a i) [<=] Zero [<=] f (b i)]. *)
84 inline cic:/CoRN/reals/IVT/f_a.var.
86 inline cic:/CoRN/reals/IVT/f_b.var.
88 inline cic:/CoRN/reals/IVT/Cnested_intervals_zero.con.
98 (*#* ** Bissections *)
100 inline cic:/CoRN/reals/IVT/f.var.
102 inline cic:/CoRN/reals/IVT/f_apzero_interval.var.
104 inline cic:/CoRN/reals/IVT/a.var.
106 inline cic:/CoRN/reals/IVT/b.var.
108 inline cic:/CoRN/reals/IVT/a_b.var.
110 inline cic:/CoRN/reals/IVT/f_a.var.
112 inline cic:/CoRN/reals/IVT/f_b.var.
115 %\begin{convention}% Let [Small] denote [Two[/]ThreeNZ], [lft] be [(Two[*]a[+]b) [/]ThreeNZ] and [rht] be [(a[+]Two[*]b) [/]ThreeNZ].
121 inline cic:/CoRN/reals/IVT/Small.con.
123 inline cic:/CoRN/reals/IVT/lft.con.
125 inline cic:/CoRN/reals/IVT/rht.con.
129 inline cic:/CoRN/reals/IVT/a_lft.con.
131 inline cic:/CoRN/reals/IVT/rht_b.con.
133 inline cic:/CoRN/reals/IVT/lft_rht.con.
135 inline cic:/CoRN/reals/IVT/smaller_lft.con.
137 inline cic:/CoRN/reals/IVT/smaller_rht.con.
140 Hint Resolve smaller_lft smaller_rht: algebra.
143 inline cic:/CoRN/reals/IVT/Cbisect'.con.
150 Section Bisect_Interval.
153 inline cic:/CoRN/reals/IVT/f.var.
155 inline cic:/CoRN/reals/IVT/C_f_apzero_interval.var.
159 inline cic:/CoRN/reals/IVT/Small.con.
163 inline cic:/CoRN/reals/IVT/bisect_interval.ind.
165 inline cic:/CoRN/reals/IVT/Cbisect_exists.con.
167 inline cic:/CoRN/reals/IVT/bisect.con.
169 inline cic:/CoRN/reals/IVT/bisect_prop.con.
179 (*#* ** IVT for operations
180 Same conventions as before.
183 inline cic:/CoRN/reals/IVT/f.var.
185 inline cic:/CoRN/reals/IVT/f_contin.var.
187 inline cic:/CoRN/reals/IVT/f_apzero_interval.var.
189 inline cic:/CoRN/reals/IVT/a.var.
191 inline cic:/CoRN/reals/IVT/b.var.
193 inline cic:/CoRN/reals/IVT/a_b.var.
195 inline cic:/CoRN/reals/IVT/f_a.var.
197 inline cic:/CoRN/reals/IVT/f_b.var.
201 inline cic:/CoRN/reals/IVT/Small.con.
205 inline cic:/CoRN/reals/IVT/interval_sequence.con.
207 inline cic:/CoRN/reals/IVT/a_.con.
209 inline cic:/CoRN/reals/IVT/b_.con.
211 inline cic:/CoRN/reals/IVT/intervals_smaller.con.
213 inline cic:/CoRN/reals/IVT/intervals_small''.con.
215 inline cic:/CoRN/reals/IVT/intervals_small'.con.
217 inline cic:/CoRN/reals/IVT/intervals_small.con.
219 inline cic:/CoRN/reals/IVT/Civt_op.con.
229 (*#* ** IVT for polynomials *)
231 inline cic:/CoRN/reals/IVT/Civt_poly.con.