set "baseuri" "cic:/matita/CoRN-Decl/ftc/WeakIVT".
+include "CoRN.ma".
+
(* $Id: WeakIVT.v,v 1.9 2004/04/23 10:01:01 lcf Exp $ *)
(*#* printing ** %\ensuremath\times% #×# *)
(* begin hide *)
+(* NOTATION
+Infix "**" := prodT (at level 20).
+*)
+
(* end hide *)
-(* INCLUDE
-Continuity
-*)
+include "ftc/Continuity.ma".
(*#* *IVT for Partial Functions
*)
(* UNEXPORTED
-Section Lemma1.
+Section Lemma1
*)
-inline cic:/CoRN/ftc/WeakIVT/a.var.
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/Lemma1/a.var".
-inline cic:/CoRN/ftc/WeakIVT/b.var.
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/Lemma1/b.var".
-inline cic:/CoRN/ftc/WeakIVT/Hab.var.
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/Lemma1/Hab.var".
(* begin hide *)
-inline cic:/CoRN/ftc/WeakIVT/I.con.
+inline "cic:/CoRN/ftc/WeakIVT/Lemma1/I.con" "Lemma1__".
(* end hide *)
-inline cic:/CoRN/ftc/WeakIVT/F.var.
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/Lemma1/F.var".
-inline cic:/CoRN/ftc/WeakIVT/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/Lemma1/contF.var".
(*#* **First Lemmas
enough to [z].
*)
-inline cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_lft.con.
+inline "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_lft.con".
(* UNEXPORTED
-End Lemma1.
+End Lemma1
*)
(* UNEXPORTED
-Section Lemma2.
+Section Lemma2
*)
-inline cic:/CoRN/ftc/WeakIVT/a.var.
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/Lemma2/a.var".
-inline cic:/CoRN/ftc/WeakIVT/b.var.
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/Lemma2/b.var".
-inline cic:/CoRN/ftc/WeakIVT/Hab.var.
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/Lemma2/Hab.var".
(* begin hide *)
-inline cic:/CoRN/ftc/WeakIVT/I.con.
+inline "cic:/CoRN/ftc/WeakIVT/Lemma2/I.con" "Lemma2__".
(* end hide *)
-inline cic:/CoRN/ftc/WeakIVT/F.var.
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/Lemma2/F.var".
-inline cic:/CoRN/ftc/WeakIVT/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/Lemma2/contF.var".
(*#*
If [f(b) [<] f(a)], a similar result holds:
*)
-inline cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_rht.con.
+inline "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_rht.con".
(* UNEXPORTED
-End Lemma2.
+End Lemma2
*)
(* UNEXPORTED
-Section IVT.
+Section IVT
*)
(*#* **The IVT
converge to [x0] such that [f(x0) [=] z].
*)
-inline cic:/CoRN/ftc/WeakIVT/a.var.
+alias id "a" = "cic:/CoRN/ftc/WeakIVT/IVT/a.var".
-inline cic:/CoRN/ftc/WeakIVT/b.var.
+alias id "b" = "cic:/CoRN/ftc/WeakIVT/IVT/b.var".
-inline cic:/CoRN/ftc/WeakIVT/Hab'.var.
+alias id "Hab'" = "cic:/CoRN/ftc/WeakIVT/IVT/Hab'.var".
-inline cic:/CoRN/ftc/WeakIVT/Hab.var.
+alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/IVT/Hab.var".
(* begin hide *)
-inline cic:/CoRN/ftc/WeakIVT/I.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT/I.con" "IVT__".
(* end hide *)
-inline cic:/CoRN/ftc/WeakIVT/F.var.
+alias id "F" = "cic:/CoRN/ftc/WeakIVT/IVT/F.var".
-inline cic:/CoRN/ftc/WeakIVT/contF.var.
+alias id "contF" = "cic:/CoRN/ftc/WeakIVT/IVT/contF.var".
(* begin hide *)
-inline cic:/CoRN/ftc/WeakIVT/incF.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT/incF.con" "IVT__".
(* end hide *)
(* begin show *)
-inline cic:/CoRN/ftc/WeakIVT/incrF.var.
+alias id "incrF" = "cic:/CoRN/ftc/WeakIVT/IVT/incrF.var".
(* end show *)
(* begin hide *)
-inline cic:/CoRN/ftc/WeakIVT/Ha.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT/Ha.con" "IVT__".
-inline cic:/CoRN/ftc/WeakIVT/Hb.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT/Hb.con" "IVT__".
-inline cic:/CoRN/ftc/WeakIVT/HFab'.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT/HFab'.con" "IVT__".
(* end hide *)
(* begin show *)
-inline cic:/CoRN/ftc/WeakIVT/z.var.
+alias id "z" = "cic:/CoRN/ftc/WeakIVT/IVT/z.var".
-inline cic:/CoRN/ftc/WeakIVT/Haz.var.
+alias id "Haz" = "cic:/CoRN/ftc/WeakIVT/IVT/Haz.var".
-inline cic:/CoRN/ftc/WeakIVT/Hzb.var.
+alias id "Hzb" = "cic:/CoRN/ftc/WeakIVT/IVT/Hzb.var".
(* end show *)
and [x' [<=] z [<=] y'].
*)
-inline cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con".
(* end hide *)
We now iterate this construction.
*)
-inline cic:/CoRN/ftc/WeakIVT/IVT_aux_seq_type.ind.
+inline "cic:/CoRN/ftc/WeakIVT/IVT_aux_seq_type.ind".
-inline cic:/CoRN/ftc/WeakIVT/IVT_iter.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT_iter.con".
-inline cic:/CoRN/ftc/WeakIVT/IVT_seq.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT_seq.con".
(*#*
We now define the sequences built from this iteration, starting with [a] and [b].
*)
-inline cic:/CoRN/ftc/WeakIVT/a_seq.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq.con".
-inline cic:/CoRN/ftc/WeakIVT/b_seq.con.
+inline "cic:/CoRN/ftc/WeakIVT/b_seq.con".
-inline cic:/CoRN/ftc/WeakIVT/a_seq_I.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq_I.con".
-inline cic:/CoRN/ftc/WeakIVT/b_seq_I.con.
+inline "cic:/CoRN/ftc/WeakIVT/b_seq_I.con".
-inline cic:/CoRN/ftc/WeakIVT/a_seq_less_b_seq.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq_less_b_seq.con".
-inline cic:/CoRN/ftc/WeakIVT/a_seq_leEq_z.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq_leEq_z.con".
-inline cic:/CoRN/ftc/WeakIVT/z_leEq_b_seq.con.
+inline "cic:/CoRN/ftc/WeakIVT/z_leEq_b_seq.con".
-inline cic:/CoRN/ftc/WeakIVT/a_seq_mon.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq_mon.con".
-inline cic:/CoRN/ftc/WeakIVT/b_seq_mon.con.
+inline "cic:/CoRN/ftc/WeakIVT/b_seq_mon.con".
-inline cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist_n.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist_n.con".
-inline cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist.con".
-inline cic:/CoRN/ftc/WeakIVT/a_seq_Cauchy.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq_Cauchy.con".
-inline cic:/CoRN/ftc/WeakIVT/b_seq_Cauchy.con.
+inline "cic:/CoRN/ftc/WeakIVT/b_seq_Cauchy.con".
-inline cic:/CoRN/ftc/WeakIVT/xa.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT/xa.con" "IVT__".
-inline cic:/CoRN/ftc/WeakIVT/xb.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT/xb.con" "IVT__".
-inline cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_lim.con.
+inline "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_lim.con".
-inline cic:/CoRN/ftc/WeakIVT/xa_in_interval.con.
+inline "cic:/CoRN/ftc/WeakIVT/xa_in_interval.con".
-inline cic:/CoRN/ftc/WeakIVT/IVT_I.con.
+inline "cic:/CoRN/ftc/WeakIVT/IVT_I.con".
(* UNEXPORTED
-End IVT.
+End IVT
*)