X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Fftc%2FWeakIVT.ma;h=e22afe085688b11ea956ed33d50ef2d242a7fbac;hb=2951babfd31047ac057714130157da2bc36e906e;hp=a66df65e1d0eb97c54e6780271cfb01ea25fd597;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma b/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma index a66df65e1..e22afe085 100644 --- a/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma +++ b/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma @@ -16,17 +16,21 @@ 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 @@ -40,24 +44,24 @@ will prove them here. *) (* 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 @@ -70,44 +74,44 @@ We begin by proving that, if [f(a) [<] f(b)], then for every [y] in 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 @@ -118,53 +122,53 @@ these assumptions, we can build two sequences of values which 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 *) @@ -173,7 +177,7 @@ we can find [x' [<] y'] such that $|x'-y'|=\frac23|x-y|$#|x'-y'|=2/3|x-y|# and [x' [<=] z [<=] y']. *) -inline cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con. +inline "cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con". (* end hide *) @@ -181,53 +185,53 @@ inline cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con. 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 *)