definition makes this possible.
*)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/subset.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/subset.con" as definition.
(*#*
The core of our work will revolve around the following fundamental
with proving the main properties of this equality relation.
*)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq.con" as definition.
(*#*
Notice that, because the quantification over the proofs is universal,
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__" as definition.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__" as definition.
(* end hide *)
this definition:
*)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/included_IR.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/included_IR.con" as lemma.
(* UNEXPORTED
End Equality_Results
If two function coincide on a given subset then they coincide in any smaller subset.
*)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/included_Feq.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/included_Feq.con" as lemma.
(* UNEXPORTED
End Some_More
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__" as definition.
(* end hide *)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con" as definition.
(*#*
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].
(* end show *)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con" as lemma.
(* UNEXPORTED
End Definitions
alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Q.var".
-inline procedural "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con" as lemma.
(*#*
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 procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con" as definition.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con" as definition.
(*#*
An immediate consequence:
*)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con" as lemma.
(* UNEXPORTED
End Away_from_Zero
alias id "H" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/H.var".
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con" as lemma.
(* UNEXPORTED
End Feq_Equivalence
alias id "G'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G'.var".
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con" as lemma.
(*#*
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 procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con" as lemma.
(*#*
The image of a set is extensional.
*)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con" as lemma.
(* UNEXPORTED
End Operations
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__" as definition.
(* end hide *)
alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Hf.var".
-inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con" as lemma.
alias id "n" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/n.var".
alias id "H'" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H'.var".
-inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con" as lemma.
(* UNEXPORTED
End Nth_Power
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__" as definition.
(* end hide *)
alias id "incF" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/incF.var".
-inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con" as lemma.
-inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con".
+inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con" as lemma.
(* UNEXPORTED
End Strong_Nth_Power