Section Lemmas
*)
-inline procedural "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__".
+inline procedural "cic:/CoRN/ftc/Integral/Lemmas/Sumx_wd_weird.con" "Lemmas__" as definition.
-inline procedural "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con".
+inline procedural "cic:/CoRN/ftc/Integral/Sumx_weird_lemma.con" as lemma.
(* UNEXPORTED
End Lemmas
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__".
+inline procedural "cic:/CoRN/ftc/Integral/Integral/I.con" "Integral__" as definition.
alias id "F" = "cic:/CoRN/ftc/Integral/Integral/F.var".
alias id "contF" = "cic:/CoRN/ftc/Integral/Integral/contF.var".
-inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__".
+inline procedural "cic:/CoRN/ftc/Integral/Integral/contF'.con" "Integral__" as definition.
(* end hide *)
Section Darboux_Sum
*)
-inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_seq.con" as definition.
-inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con".
+inline procedural "cic:/CoRN/ftc/Integral/Cauchy_Darboux_Seq.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral.con" as definition.
(* UNEXPORTED
End Darboux_Sum
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__".
+inline procedural "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/d.con" "Integral__Integral_Thm__" as definition.
(* end hide *)
alias id "incF" = "cic:/CoRN/ftc/Integral/Integral/Integral_Thm/incF.var".
-inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_Sum_conv_integral.con" as lemma.
(* UNEXPORTED
End Integral_Thm
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__".
+inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/I.con" "Basic_Properties__" as definition.
(* end hide *)
alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Well_Definedness/contG.var".
-inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_strext.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_strext'.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_wd.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_wd'.con" as lemma.
(* UNEXPORTED
End Well_Definedness
The integral is a linear and monotonous function; in order to prove these facts we also need the important equalities $\int_a^bdx=b-a$#∫<sub>a</sub><sup>b</sup>dx=b-a# and $\int_a^af(x)dx=0$#∫<sub>a</sub><sup>a</sup>=0#.
*)
-inline procedural "cic:/CoRN/ftc/Integral/integral_one.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_one.con" as lemma.
alias id "F" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/F.var".
alias id "contG" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity/contG.var".
-inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_comm_scal.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_plus.con" as lemma.
(* UNEXPORTED
Transparent Even_Partition.
*)
-inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_empty.con" as lemma.
(* UNEXPORTED
End Linearity_and_Monotonicity
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__".
+inline procedural "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/h.con" "Basic_Properties__Linearity_and_Monotonicity'__" as definition.
(* end hide *)
alias id "contH" = "cic:/CoRN/ftc/Integral/Basic_Properties/Linearity_and_Monotonicity'/contH.var".
-inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/linear_integral.con" as lemma.
(* UNEXPORTED
Opaque nring.
*)
-inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/monotonous_integral.con" as lemma.
(* UNEXPORTED
Transparent nring.
As corollaries we can calculate integrals of group operations applied to functions.
*)
-inline procedural "cic:/CoRN/ftc/Integral/integral_const.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_const.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_minus.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_inv.con" as lemma.
(*#*
We can also bound integrals by bounding the integrated functions.
*)
-inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/lb_integral.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/ub_integral.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_leEq_norm.con" as lemma.
(* UNEXPORTED
End Corollaries
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux.con" as lemma.
(* end hide *)
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_fun.con" as definition.
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjf_1.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjf_2.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjf_2'.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjf_3.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf1.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_prf2.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_start.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_finish.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/partition_join.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join.con" as definition.
(* end hide *)
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_aux'.con" as lemma.
(* end hide *)
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_pts.con" as definition.
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjp_1.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjp_2.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con".
+inline procedural "cic:/CoRN/ftc/Integral/pjp_3.con" as lemma.
(* end hide *)
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_in_partition.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_Pts_wd.con" as lemma.
(* UNEXPORTED
Opaque partition_join.
Transparent minus.
*)
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_Sum_lemma.con" as lemma.
-inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con".
+inline procedural "cic:/CoRN/ftc/Integral/partition_join_mesh.con" as lemma.
(* UNEXPORTED
End Partition_Join
Opaque Even_Partition.
*)
-inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_plus_integral.con" as lemma.
(* UNEXPORTED
End Integral_Sum
The following are simple consequences of this result and of previous ones.
*)
-inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_less_norm.con" as lemma.
(* end hide *)
-inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con".
+inline procedural "cic:/CoRN/ftc/Integral/integral_gt_zero.con" as lemma.
(* end hide *)