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 *********************)
19 (* $Id: StrongIVT.v,v 1.5 2004/04/23 10:01:01 lcf Exp $ *)
21 include "ftc/WeakIVT.ma".
23 include "ftc/CalculusTheorems.ma".
29 (*#* ** Strong IVT for partial functions
31 The IVT can be generalized to arbitrary partial functions; in the first
32 part, we will simply do that, repeating the previous construction.
34 The same notations and conventions apply as before.
37 alias id "a" = "cic:/CoRN/ftc/StrongIVT/IVT'/a.var".
39 alias id "b" = "cic:/CoRN/ftc/StrongIVT/IVT'/b.var".
41 alias id "Hab'" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hab'.var".
43 alias id "Hab" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hab.var".
47 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/I.con" "IVT'__" as definition.
49 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/I'.con" "IVT'__" as definition.
53 alias id "F" = "cic:/CoRN/ftc/StrongIVT/IVT'/F.var".
55 alias id "contF" = "cic:/CoRN/ftc/StrongIVT/IVT'/contF.var".
59 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/incF.con" "IVT'__" as definition.
65 alias id "incrF" = "cic:/CoRN/ftc/StrongIVT/IVT'/incrF.var".
71 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/Ha.con" "IVT'__" as definition.
73 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/Hb.con" "IVT'__" as definition.
75 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/HFab'.con" "IVT'__" as definition.
81 alias id "z" = "cic:/CoRN/ftc/StrongIVT/IVT'/z.var".
83 alias id "Haz" = "cic:/CoRN/ftc/StrongIVT/IVT'/Haz.var".
85 alias id "Hzb" = "cic:/CoRN/ftc/StrongIVT/IVT'/Hzb.var".
89 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'_seq_lemma.con" as lemma.
93 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'_aux_seq_type.ind".
95 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'_iter.con" as definition.
97 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'_seq.con" as definition.
99 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq.con" as definition.
101 inline procedural "cic:/CoRN/ftc/StrongIVT/b'_seq.con" as definition.
103 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq_I.con" as definition.
105 inline procedural "cic:/CoRN/ftc/StrongIVT/b'_seq_I.con" as definition.
107 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq_less_b'_seq.con" as lemma.
109 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq_less_z.con" as lemma.
111 inline procedural "cic:/CoRN/ftc/StrongIVT/z_less_b'_seq.con" as lemma.
113 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq_mon.con" as lemma.
115 inline procedural "cic:/CoRN/ftc/StrongIVT/b'_seq_mon.con" as lemma.
117 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_dist_n.con" as lemma.
119 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_dist.con" as lemma.
121 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq_Cauchy.con" as lemma.
123 inline procedural "cic:/CoRN/ftc/StrongIVT/b'_seq_Cauchy.con" as lemma.
125 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/xa.con" "IVT'__" as definition.
127 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'/xb.con" "IVT'__" as definition.
129 inline procedural "cic:/CoRN/ftc/StrongIVT/a'_seq_b'_seq_lim.con" as lemma.
131 inline procedural "cic:/CoRN/ftc/StrongIVT/xa'_in_interval.con" as lemma.
133 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'_I.con" as lemma.
139 (*#* **Other formulations
141 We now generalize the various statements of the intermediate value
142 theorem to more widely applicable forms.
145 inline procedural "cic:/CoRN/ftc/StrongIVT/Weak_IVT.con" as lemma.
147 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT_inc.con" as lemma.
153 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT_dec.con" as lemma.
155 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'_inc.con" as lemma.
161 inline procedural "cic:/CoRN/ftc/StrongIVT/IVT'_dec.con" as lemma.