set "baseuri" "cic:/matita/CoRN-Decl/ftc/FunctSums".
+include "CoRN.ma".
+
(* $Id: FunctSums.v,v 1.5 2004/04/23 10:00:59 lcf Exp $ *)
(*#* printing FSum0 %\ensuremath{\sum_0}% #∑<sub>0</sub># *)
(*#* printing FSumx %\ensuremath{\sum'}% #∑'&*)
-(* INCLUDE
-CSumsReals
-*)
+include "reals/CSumsReals.ma".
-(* INCLUDE
-PartFunEquality
-*)
+include "ftc/PartFunEquality.ma".
(*#* *Sums of Functions
( [FSum]).
*)
-inline cic:/CoRN/ftc/FunctSums/FSum0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0.con".
-inline cic:/CoRN/ftc/FunctSums/FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum.con".
(*#*
Although [FSum] is here defined directly, it has the same relationship
those results.
*)
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0.con".
-inline cic:/CoRN/ftc/FunctSums/FSum0_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_wd.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_one.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_one.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_first.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_first.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_last.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_last.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_last'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_last'.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_wd.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/inv_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/inv_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_wd'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_wd'.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_resp_less.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_resp_less.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con".
(*#*
Also important is the case when we have a finite family
to use the [FSumx] operator.
*)
-inline cic:/CoRN/ftc/FunctSums/FSumx.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx.con".
(*#*
This operator is well defined, as expected.
*)
-inline cic:/CoRN/ftc/FunctSums/FSumx_wd.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_wd.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_wd'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_wd'.con".
(*#*
As was already the case for [Sumx], in many cases we will need to
function $f_i$#f<sub>i</sub>#.
*)
-inline cic:/CoRN/ftc/FunctSums/ext_fun_seq.con.
+inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq.con".
-inline cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con.
+inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con".
(* UNEXPORTED
Implicit Arguments ext_fun_seq [n].
Under these assumptions, we can characterize the domain and the value of the sum function from the domains and values of the summands:
*)
-inline cic:/CoRN/ftc/FunctSums/FSumx_pred.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_pred.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_pred'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_pred'.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_char.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_char.con".
(*#*
As we did for arbitrary groups, it is often useful to rewrite this sums as ordinary sums.
*)
-inline cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_lt.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_lt.con".
-inline cic:/CoRN/ftc/FunctSums/FSumx_le.con.
+inline "cic:/CoRN/ftc/FunctSums/FSumx_le.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con".
(*#*
Some useful lemmas follow.
*)
-inline cic:/CoRN/ftc/FunctSums/FSum0_0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_0.con".
-inline cic:/CoRN/ftc/FunctSums/FSum0_S.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum0_S.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_0.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_0.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_S.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_S.con".
-inline cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con.
+inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con".