X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FMoreIntervals.ma;h=30bf4b4231c2c7d5133e3c5279d9c08eb9ad9658;hb=55e5bef77f163b29feeb9ad4e83376c5aa301297;hp=c3abe0aa650ed8b1fb9a8a823ca84b77b1be44ad;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma index c3abe0aa6..30bf4b423 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/MoreIntervals". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: MoreIntervals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *) @@ -27,7 +27,7 @@ Opaque Min Max. *) (* UNEXPORTED -Section Intervals. +Section Intervals *) (*#* printing realline %\ensuremath{\RR}% #(-∞,+∞)# *) @@ -111,7 +111,7 @@ inline "cic:/CoRN/ftc/MoreIntervals/iprop.con". (* begin hide *) -coercion "cic:/matita/CoRN-Decl/ftc/MoreIntervals/iprop.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/ftc/MoreIntervals/iprop.con 0 (* compounds *). (* end hide *) @@ -186,7 +186,7 @@ Finally, all intervals are characterized by well defined predicates. inline "cic:/CoRN/ftc/MoreIntervals/iprop_wd.con". (* UNEXPORTED -End Intervals. +End Intervals *) (* UNEXPORTED @@ -198,11 +198,11 @@ Implicit Arguments Rend [I]. *) (* UNEXPORTED -Section Compact_Constructions. +Section Compact_Constructions *) (* UNEXPORTED -Section Single_Compact_Interval. +Section Single_Compact_Interval *) (*#* **Constructions with Compact Intervals @@ -216,13 +216,13 @@ such that [P(x)] holds. %\end{convention}% *) -inline "cic:/CoRN/ftc/MoreIntervals/P.var". +alias id "P" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/P.var". -inline "cic:/CoRN/ftc/MoreIntervals/wdP.var". +alias id "wdP" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/wdP.var". -inline "cic:/CoRN/ftc/MoreIntervals/x.var". +alias id "x" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/x.var". -inline "cic:/CoRN/ftc/MoreIntervals/Hx.var". +alias id "Hx" = "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Single_Compact_Interval/Hx.var". inline "cic:/CoRN/ftc/MoreIntervals/compact_single.con". @@ -237,7 +237,7 @@ inline "cic:/CoRN/ftc/MoreIntervals/compact_single_pt.con". inline "cic:/CoRN/ftc/MoreIntervals/compact_single_inc.con". (* UNEXPORTED -End Single_Compact_Interval. +End Single_Compact_Interval *) (*#* @@ -255,34 +255,34 @@ I$#x∈[a,b]⊆I#. *) (* UNEXPORTED -Section Proper_Compact_with_One_or_Two_Points. +Section Proper_Compact_with_One_or_Two_Points *) (* begin hide *) -inline "cic:/CoRN/ftc/MoreIntervals/cip1'.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip1''.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip1'''.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip1''''.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip1''''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip2.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip2'.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip2''.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip2'''.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip2'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip3.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip3'.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip3''.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". -inline "cic:/CoRN/ftc/MoreIntervals/cip3'''.con". +inline "cic:/CoRN/ftc/MoreIntervals/Compact_Constructions/Proper_Compact_with_One_or_Two_Points/cip3'''.con" "Compact_Constructions__Proper_Compact_with_One_or_Two_Points__". (* end hide *) @@ -350,7 +350,7 @@ inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_x_rht.con". inline "cic:/CoRN/ftc/MoreIntervals/compact_in_interval_y_rht.con". (* UNEXPORTED -End Proper_Compact_with_One_or_Two_Points. +End Proper_Compact_with_One_or_Two_Points *) (*#* @@ -370,11 +370,11 @@ $[a,b]\subseteq[a',b']\subseteq J$#[a,b]⊆[a',b']⊆J#. inline "cic:/CoRN/ftc/MoreIntervals/compact_proper_in_interval.con". (* UNEXPORTED -End Compact_Constructions. +End Compact_Constructions *) (* UNEXPORTED -Section Functions. +Section Functions *) (*#* **Properties of Functions in Intervals @@ -389,9 +389,9 @@ previously defined concepts. %\end{convention}% *) -inline "cic:/CoRN/ftc/MoreIntervals/n.var". +alias id "n" = "cic:/CoRN/ftc/MoreIntervals/Functions/n.var". -inline "cic:/CoRN/ftc/MoreIntervals/I.var". +alias id "I" = "cic:/CoRN/ftc/MoreIntervals/Functions/I.var". inline "cic:/CoRN/ftc/MoreIntervals/Continuous.con". @@ -404,11 +404,11 @@ inline "cic:/CoRN/ftc/MoreIntervals/Derivative_n.con". inline "cic:/CoRN/ftc/MoreIntervals/Diffble_n.con". (* UNEXPORTED -End Functions. +End Functions *) (* UNEXPORTED -Section Reflexivity_Properties. +Section Reflexivity_Properties *) (*#* @@ -428,11 +428,11 @@ inline "cic:/CoRN/ftc/MoreIntervals/Diffble_Int.con". inline "cic:/CoRN/ftc/MoreIntervals/Int_Diffble.con". (* UNEXPORTED -End Reflexivity_Properties. +End Reflexivity_Properties *) (* UNEXPORTED -Section Lemmas. +Section Lemmas *) (*#* @@ -446,7 +446,7 @@ inline "cic:/CoRN/ftc/MoreIntervals/included_Feq''.con". inline "cic:/CoRN/ftc/MoreIntervals/included_Feq'.con". (* UNEXPORTED -End Lemmas. +End Lemmas *) (* UNEXPORTED