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
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
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,
*)
(* UNEXPORTED
-End Definitions.
+End Definitions
*)
(* UNEXPORTED
-Section Equality_Results.
+Section Equality_Results
*)
(*#* **Properties of Inclusion
%\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
*)
(* 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
%\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].
(* 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
*)
(*#*
%\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
(* end hide *)
(* UNEXPORTED
-Section More_on_Equality.
+Section More_on_Equality
*)
(*#* **Properties of Equality
%\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.
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
%\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
*)
(*#*
%\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
*)