X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Fftc%2FPartFunEquality.ma;h=9771d16f2b7abeba20d66dc2222281f40a8fd29e;hb=55e5bef77f163b29feeb9ad4e83376c5aa301297;hp=0ca5ba98a84281b6556bb80279dee6a375c6ce11;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma b/helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma index 0ca5ba98a..9771d16f2 100644 --- a/helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma +++ b/helm/software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma @@ -16,20 +16,18 @@ set "baseuri" "cic:/matita/CoRN-Decl/ftc/PartFunEquality". +include "CoRN.ma". + (* $Id: PartFunEquality.v,v 1.8 2004/04/23 10:00:59 lcf Exp $ *) (*#* printing Feq %\ensuremath{\approx}% #≈# *) -(* INCLUDE -Intervals -*) +include "reals/Intervals.ma". -(* INCLUDE -DiffTactics1 -*) +include "tactics/DiffTactics1.ma". (* UNEXPORTED -Section Definitions. +Section Definitions *) (*#* *Equality of Partial Functions @@ -42,7 +40,7 @@ given predicate rather than to the predicate itself. The following definition makes this possible. *) -inline cic:/CoRN/ftc/PartFunEquality/subset.con. +inline "cic:/CoRN/ftc/PartFunEquality/subset.con". (*#* The core of our work will revolve around the following fundamental @@ -54,7 +52,7 @@ it is easier to consider a generic case%.}%. This file is concerned with proving the main properties of this equality relation. *) -inline cic:/CoRN/ftc/PartFunEquality/Feq.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq.con". (*#* Notice that, because the quantification over the proofs is universal, @@ -73,11 +71,11 @@ than in an existentially quantified one. *) (* UNEXPORTED -End Definitions. +End Definitions *) (* UNEXPORTED -Section Equality_Results. +Section Equality_Results *) (*#* **Properties of Inclusion @@ -89,35 +87,35 @@ by [P] and [Q], respectively, the domains of [F] and [G]. %\end{convention}% *) -inline cic:/CoRN/ftc/PartFunEquality/I.var. +alias id "I" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/I.var". -inline cic:/CoRN/ftc/PartFunEquality/F.var. +alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/F.var". -inline cic:/CoRN/ftc/PartFunEquality/G.var. +alias id "G" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/G.var". (* begin hide *) -inline cic:/CoRN/ftc/PartFunEquality/P.con. +inline "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__". -inline cic:/CoRN/ftc/PartFunEquality/Q.con. +inline "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__". (* end hide *) -inline cic:/CoRN/ftc/PartFunEquality/R.var. +alias id "R" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/R.var". (*#* We start with two lemmas which make it much easier to prove and use this definition: *) -inline cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con. +inline "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con". -inline cic:/CoRN/ftc/PartFunEquality/included_IR.con. +inline "cic:/CoRN/ftc/PartFunEquality/included_IR.con". (* UNEXPORTED -End Equality_Results. +End Equality_Results *) (* UNEXPORTED @@ -125,25 +123,25 @@ Hint Resolve included_IR : included. *) (* UNEXPORTED -Section Some_More. +Section Some_More *) (*#* If two function coincide on a given subset then they coincide in any smaller subset. *) -inline cic:/CoRN/ftc/PartFunEquality/included_Feq.con. +inline "cic:/CoRN/ftc/PartFunEquality/included_Feq.con". (* UNEXPORTED -End Some_More. +End Some_More *) (* UNEXPORTED -Section Away_from_Zero. +Section Away_from_Zero *) (* UNEXPORTED -Section Definitions. +Section Definitions *) (*#* **Away from Zero @@ -158,17 +156,17 @@ the domain of [F]. %\end{convention}% *) -inline cic:/CoRN/ftc/PartFunEquality/I.var. +alias id "I" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/I.var". -inline cic:/CoRN/ftc/PartFunEquality/F.var. +alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/F.var". (* begin hide *) -inline cic:/CoRN/ftc/PartFunEquality/P.con. +inline "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__". (* end hide *) -inline cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con. +inline "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con". (*#* If [F] is bounded away from zero in [I] then [F] is necessarily apart from zero in [I]; also this means that [I] is included in the domain of [{1/}F]. @@ -176,18 +174,18 @@ If [F] is bounded away from zero in [I] then [F] is necessarily apart from zero (* begin show *) -inline cic:/CoRN/ftc/PartFunEquality/Hf.var. +alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/Hf.var". (* end show *) -inline cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con. +inline "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con". -inline cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con. +inline "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con". -inline cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con. +inline "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con". (* UNEXPORTED -End Definitions. +End Definitions *) (*#* @@ -197,34 +195,34 @@ Boundedness away from zero is preserved through restriction of the set. %\end{convention}% *) -inline cic:/CoRN/ftc/PartFunEquality/F.var. +alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/F.var". -inline cic:/CoRN/ftc/PartFunEquality/P.var. +alias id "P" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/P.var". -inline cic:/CoRN/ftc/PartFunEquality/Q.var. +alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Q.var". -inline cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con. +inline "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con". -inline cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con. +inline "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con". (*#* A function is said to be bounded away from zero everywhere if it is bounded away from zero in every compact subinterval of its domain; a similar definition is made for arbitrary sets, which will be necessary for future work. *) -inline cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con. +inline "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con". -inline cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con. +inline "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con". (*#* An immediate consequence: *) -inline cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con. +inline "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con". -inline cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con. +inline "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con". (* UNEXPORTED -End Away_from_Zero. +End Away_from_Zero *) (* UNEXPORTED @@ -251,7 +249,7 @@ Ltac FEQ := apply eq_imp_Feq; (* end hide *) (* UNEXPORTED -Section More_on_Equality. +Section More_on_Equality *) (*#* **Properties of Equality @@ -263,61 +261,61 @@ partial functions. %\end{convention}% *) -inline cic:/CoRN/ftc/PartFunEquality/I.var. +alias id "I" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/I.var". (* UNEXPORTED -Section Feq_Equivalence. +Section Feq_Equivalence *) -inline cic:/CoRN/ftc/PartFunEquality/F.var. +alias id "F" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/F.var". -inline cic:/CoRN/ftc/PartFunEquality/G.var. +alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/G.var". -inline cic:/CoRN/ftc/PartFunEquality/H.var. +alias id "H" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/H.var". -inline cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con". (* UNEXPORTED -End Feq_Equivalence. +End Feq_Equivalence *) (* UNEXPORTED -Section Operations. +Section Operations *) (*#* Also it is preserved through application of functional constructors and restriction. *) -inline cic:/CoRN/ftc/PartFunEquality/F.var. +alias id "F" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F.var". -inline cic:/CoRN/ftc/PartFunEquality/F'.var. +alias id "F'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/F'.var". -inline cic:/CoRN/ftc/PartFunEquality/G.var. +alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G.var". -inline cic:/CoRN/ftc/PartFunEquality/G'.var. +alias id "G'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G'.var". -inline cic:/CoRN/ftc/PartFunEquality/Feq_plus.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_inv.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_minus.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_mult.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_nth.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_recip.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_div.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_div.con". -inline cic:/CoRN/ftc/PartFunEquality/Feq_div'.con. +inline "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con". (*#* Notice that in the case of division we only need to require boundedness away from zero for one of the functions (as they are equal); thus the two last lemmas are stated in two different ways, as according to the context one or the other condition may be easier to prove. @@ -325,24 +323,24 @@ Notice that in the case of division we only need to require boundedness away fro The restriction of a function is well defined. *) -inline cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con. +inline "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con". (*#* The image of a set is extensional. *) -inline cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con. +inline "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con". (* UNEXPORTED -End Operations. +End Operations *) (* UNEXPORTED -End More_on_Equality. +End More_on_Equality *) (* UNEXPORTED -Section Nth_Power. +Section Nth_Power *) (*#* **Nth Power @@ -357,34 +355,34 @@ equality relation. %\end{convention}% *) -inline cic:/CoRN/ftc/PartFunEquality/F.var. +alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/F.var". (* begin hide *) -inline cic:/CoRN/ftc/PartFunEquality/P.con. +inline "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__". (* end hide *) -inline cic:/CoRN/ftc/PartFunEquality/Q.var. +alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Q.var". -inline cic:/CoRN/ftc/PartFunEquality/H.var. +alias id "H" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H.var". -inline cic:/CoRN/ftc/PartFunEquality/Hf.var. +alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Hf.var". -inline cic:/CoRN/ftc/PartFunEquality/FNth_zero.con. +inline "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con". -inline cic:/CoRN/ftc/PartFunEquality/n.var. +alias id "n" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/n.var". -inline cic:/CoRN/ftc/PartFunEquality/H'.var. +alias id "H'" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H'.var". -inline cic:/CoRN/ftc/PartFunEquality/FNth_mult.con. +inline "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con". (* UNEXPORTED -End Nth_Power. +End Nth_Power *) (* UNEXPORTED -Section Strong_Nth_Power. +Section Strong_Nth_Power *) (*#* @@ -393,27 +391,27 @@ is included in the domain of [F]. %\end{convention}% *) -inline cic:/CoRN/ftc/PartFunEquality/a.var. +alias id "a" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/a.var". -inline cic:/CoRN/ftc/PartFunEquality/b.var. +alias id "b" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/b.var". -inline cic:/CoRN/ftc/PartFunEquality/Hab.var. +alias id "Hab" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/Hab.var". (* begin hide *) -inline cic:/CoRN/ftc/PartFunEquality/I.con. +inline "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__". (* end hide *) -inline cic:/CoRN/ftc/PartFunEquality/F.var. +alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/F.var". -inline cic:/CoRN/ftc/PartFunEquality/incF.var. +alias id "incF" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/incF.var". -inline cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con. +inline "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con". -inline cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con. +inline "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con". (* UNEXPORTED -End Strong_Nth_Power. +End Strong_Nth_Power *)