X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Freals%2FMax_AbsIR.ma;h=6c3b89c8d26e937db963d80bc0e5d54368604a06;hb=5e01cba364607e7937aec2e359c34f049bb0f108;hp=7a1e016b4c3fe2a6e4b1f71dca0e232c8c504f2d;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma b/helm/software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma index 7a1e016b4..6c3b89c8d 100644 --- a/helm/software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma +++ b/helm/software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma @@ -16,22 +16,22 @@ set "baseuri" "cic:/matita/CoRN-Decl/reals/Max_AbsIR". +include "CoRN.ma". + (* $Id: Max_AbsIR.v,v 1.13 2004/04/23 10:01:04 lcf Exp $ *) (*#* printing Max %\ensuremath{\max}% *) (*#* printing Min %\ensuremath{\min}% *) -(* INCLUDE -CauchySeq -*) +include "reals/CauchySeq.ma". (* UNEXPORTED -Section Maximum. +Section Maximum *) (* UNEXPORTED -Section Max_function. +Section Max_function *) (*#* ** Maximum, Minimum and Absolute Value @@ -42,19 +42,19 @@ Let [x] and [y] be reals %\end{convention}% *) -inline cic:/CoRN/reals/Max_AbsIR/x.var. +inline "cic:/CoRN/reals/Max_AbsIR/Maximum/Max_function/x.var" "Maximum__Max_function__". -inline cic:/CoRN/reals/Max_AbsIR/y.var. +inline "cic:/CoRN/reals/Max_AbsIR/Maximum/Max_function/y.var" "Maximum__Max_function__". -inline cic:/CoRN/reals/Max_AbsIR/Max_seq.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_seq.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_seq_char.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_seq_char.con". -inline cic:/CoRN/reals/Max_AbsIR/Cauchy_Max_seq.con. +inline "cic:/CoRN/reals/Max_AbsIR/Cauchy_Max_seq.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_CauchySeq.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_CauchySeq.con". -inline cic:/CoRN/reals/Max_AbsIR/MAX.con. +inline "cic:/CoRN/reals/Max_AbsIR/MAX.con". (*#* Constructively, the elementary properties of the maximum function are: @@ -70,64 +70,64 @@ With strong extensionality, we can make the binary operation [Max]. (So [Max] is [MAX] coupled with some proofs.) *) -inline cic:/CoRN/reals/Max_AbsIR/lft_leEq_MAX.con. +inline "cic:/CoRN/reals/Max_AbsIR/lft_leEq_MAX.con". -inline cic:/CoRN/reals/Max_AbsIR/rht_leEq_MAX.con. +inline "cic:/CoRN/reals/Max_AbsIR/rht_leEq_MAX.con". -inline cic:/CoRN/reals/Max_AbsIR/less_MAX_imp.con. +inline "cic:/CoRN/reals/Max_AbsIR/less_MAX_imp.con". (* UNEXPORTED -End Max_function. +End Max_function *) -inline cic:/CoRN/reals/Max_AbsIR/MAX_strext.con. +inline "cic:/CoRN/reals/Max_AbsIR/MAX_strext.con". -inline cic:/CoRN/reals/Max_AbsIR/MAX_wd.con. +inline "cic:/CoRN/reals/Max_AbsIR/MAX_wd.con". (* UNEXPORTED -Section properties_of_Max. +Section properties_of_Max *) (*#* *** Maximum *) -inline cic:/CoRN/reals/Max_AbsIR/Max.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_wd_unfolded.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_wd_unfolded.con". -inline cic:/CoRN/reals/Max_AbsIR/lft_leEq_Max.con. +inline "cic:/CoRN/reals/Max_AbsIR/lft_leEq_Max.con". -inline cic:/CoRN/reals/Max_AbsIR/rht_leEq_Max.con. +inline "cic:/CoRN/reals/Max_AbsIR/rht_leEq_Max.con". -inline cic:/CoRN/reals/Max_AbsIR/less_Max_imp.con. +inline "cic:/CoRN/reals/Max_AbsIR/less_Max_imp.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_leEq.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_leEq.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_less.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_less.con". -inline cic:/CoRN/reals/Max_AbsIR/equiv_imp_eq_max.con. +inline "cic:/CoRN/reals/Max_AbsIR/equiv_imp_eq_max.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_id.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_id.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_comm.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_comm.con". -inline cic:/CoRN/reals/Max_AbsIR/leEq_imp_Max_is_rht.con. +inline "cic:/CoRN/reals/Max_AbsIR/leEq_imp_Max_is_rht.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_is_rht_imp_leEq.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_is_rht_imp_leEq.con". -inline cic:/CoRN/reals/Max_AbsIR/Max_minus_eps_leEq.con. +inline "cic:/CoRN/reals/Max_AbsIR/Max_minus_eps_leEq.con". -inline cic:/CoRN/reals/Max_AbsIR/max_one_ap_zero.con. +inline "cic:/CoRN/reals/Max_AbsIR/max_one_ap_zero.con". -inline cic:/CoRN/reals/Max_AbsIR/pos_max_one.con. +inline "cic:/CoRN/reals/Max_AbsIR/pos_max_one.con". -inline cic:/CoRN/reals/Max_AbsIR/x_div_Max_leEq_x.con. +inline "cic:/CoRN/reals/Max_AbsIR/x_div_Max_leEq_x.con". (* UNEXPORTED -End properties_of_Max. +End properties_of_Max *) (* UNEXPORTED -End Maximum. +End Maximum *) (* UNEXPORTED @@ -135,7 +135,7 @@ Hint Resolve Max_id: algebra. *) (* UNEXPORTED -Section Minimum. +Section Minimum *) (*#* *** Mininum @@ -144,134 +144,134 @@ The minimum is defined by the formula [Min(x,y) [=] [--]Max( [--]x,[--]y)]. *) -inline cic:/CoRN/reals/Max_AbsIR/MIN.con. +inline "cic:/CoRN/reals/Max_AbsIR/MIN.con". -inline cic:/CoRN/reals/Max_AbsIR/MIN_wd.con. +inline "cic:/CoRN/reals/Max_AbsIR/MIN_wd.con". -inline cic:/CoRN/reals/Max_AbsIR/MIN_strext.con. +inline "cic:/CoRN/reals/Max_AbsIR/MIN_strext.con". -inline cic:/CoRN/reals/Max_AbsIR/Min.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_wd_unfolded.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_wd_unfolded.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_strext_unfolded.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_strext_unfolded.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_leEq_lft.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_lft.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_leEq_rht.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_rht.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_less_imp.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_less_imp.con". -inline cic:/CoRN/reals/Max_AbsIR/leEq_Min.con. +inline "cic:/CoRN/reals/Max_AbsIR/leEq_Min.con". -inline cic:/CoRN/reals/Max_AbsIR/less_Min.con. +inline "cic:/CoRN/reals/Max_AbsIR/less_Min.con". -inline cic:/CoRN/reals/Max_AbsIR/equiv_imp_eq_min.con. +inline "cic:/CoRN/reals/Max_AbsIR/equiv_imp_eq_min.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_id.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_id.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_comm.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_comm.con". -inline cic:/CoRN/reals/Max_AbsIR/leEq_imp_Min_is_lft.con. +inline "cic:/CoRN/reals/Max_AbsIR/leEq_imp_Min_is_lft.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_is_lft_imp_leEq.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_is_lft_imp_leEq.con". -inline cic:/CoRN/reals/Max_AbsIR/leEq_Min_plus_eps.con. +inline "cic:/CoRN/reals/Max_AbsIR/leEq_Min_plus_eps.con". -inline cic:/CoRN/reals/Max_AbsIR/a.var. +inline "cic:/CoRN/reals/Max_AbsIR/Minimum/a.var" "Minimum__". -inline cic:/CoRN/reals/Max_AbsIR/b.var. +inline "cic:/CoRN/reals/Max_AbsIR/Minimum/b.var" "Minimum__". -inline cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max'.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max'.con". -inline cic:/CoRN/reals/Max_AbsIR/Min3_leEq_Max3.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min3_leEq_Max3.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_less_Max.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_less_Max.con". -inline cic:/CoRN/reals/Max_AbsIR/ap_imp_Min_less_Max.con. +inline "cic:/CoRN/reals/Max_AbsIR/ap_imp_Min_less_Max.con". -inline cic:/CoRN/reals/Max_AbsIR/Min_less_Max_imp_ap.con. +inline "cic:/CoRN/reals/Max_AbsIR/Min_less_Max_imp_ap.con". (* UNEXPORTED -End Minimum. +End Minimum *) (*#**********************************) (* UNEXPORTED -Section Absolute. +Section Absolute *) (*#**********************************) (*#* *** Absolute value *) -inline cic:/CoRN/reals/Max_AbsIR/ABSIR.con. +inline "cic:/CoRN/reals/Max_AbsIR/ABSIR.con". -inline cic:/CoRN/reals/Max_AbsIR/ABSIR_strext.con. +inline "cic:/CoRN/reals/Max_AbsIR/ABSIR_strext.con". -inline cic:/CoRN/reals/Max_AbsIR/ABSIR_wd.con. +inline "cic:/CoRN/reals/Max_AbsIR/ABSIR_wd.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_wd.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_wd.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_wdl.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_wdl.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_wdr.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_wdr.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIRz_isz.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIRz_isz.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_nonneg.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_nonneg.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_pos.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_pos.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_cancel_ap_zero.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_cancel_ap_zero.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_resp_ap_zero.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_resp_ap_zero.con". -inline cic:/CoRN/reals/Max_AbsIR/leEq_AbsIR.con. +inline "cic:/CoRN/reals/Max_AbsIR/leEq_AbsIR.con". -inline cic:/CoRN/reals/Max_AbsIR/inv_leEq_AbsIR.con. +inline "cic:/CoRN/reals/Max_AbsIR/inv_leEq_AbsIR.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsSmall_e.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsSmall_e.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsSmall_imp_AbsIR.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsSmall_imp_AbsIR.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_AbsSmall.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_AbsSmall.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_imp_AbsSmall.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_imp_AbsSmall.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsSmall_transitive.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsSmall_transitive.con". -inline cic:/CoRN/reals/Max_AbsIR/zero_less_AbsIR_plus_one.con. +inline "cic:/CoRN/reals/Max_AbsIR/zero_less_AbsIR_plus_one.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_inv.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_inv.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_minus.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_minus.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_x.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_x.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_inv_x.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_inv_x.con". -inline cic:/CoRN/reals/Max_AbsIR/less_AbsIR.con. +inline "cic:/CoRN/reals/Max_AbsIR/less_AbsIR.con". -inline cic:/CoRN/reals/Max_AbsIR/leEq_distr_AbsIR.con. +inline "cic:/CoRN/reals/Max_AbsIR/leEq_distr_AbsIR.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_approach_zero.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_approach_zero.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_zero.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_zero.con". -inline cic:/CoRN/reals/Max_AbsIR/Abs_Max.con. +inline "cic:/CoRN/reals/Max_AbsIR/Abs_Max.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_str_bnd.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_str_bnd.con". -inline cic:/CoRN/reals/Max_AbsIR/AbsIR_bnd.con. +inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_bnd.con". (* UNEXPORTED -End Absolute. +End Absolute *) (* UNEXPORTED @@ -279,7 +279,7 @@ Hint Resolve AbsIRz_isz: algebra. *) (* UNEXPORTED -Section Part_Function_Max. +Section Part_Function_Max *) (*#* *** Functional Operators @@ -291,87 +291,87 @@ Let [F,G:PartIR] and denote by [P] and [Q] their respective domains. %\end{convention}% *) -inline cic:/CoRN/reals/Max_AbsIR/F.var. +inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/F.var" "Part_Function_Max__". -inline cic:/CoRN/reals/Max_AbsIR/G.var. +inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/G.var" "Part_Function_Max__". (* begin hide *) -inline cic:/CoRN/reals/Max_AbsIR/P.con. +inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/P.con" "Part_Function_Max__". -inline cic:/CoRN/reals/Max_AbsIR/Q.con. +inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/Q.con" "Part_Function_Max__". (* end hide *) -inline cic:/CoRN/reals/Max_AbsIR/part_function_Max_strext.con. +inline "cic:/CoRN/reals/Max_AbsIR/part_function_Max_strext.con". -inline cic:/CoRN/reals/Max_AbsIR/FMax.con. +inline "cic:/CoRN/reals/Max_AbsIR/FMax.con". (* UNEXPORTED -End Part_Function_Max. +End Part_Function_Max *) (* UNEXPORTED -Section Part_Function_Abs. +Section Part_Function_Abs *) -inline cic:/CoRN/reals/Max_AbsIR/F.var. +inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/F.var" "Part_Function_Abs__". -inline cic:/CoRN/reals/Max_AbsIR/G.var. +inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/G.var" "Part_Function_Abs__". (* begin hide *) -inline cic:/CoRN/reals/Max_AbsIR/P.con. +inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/P.con" "Part_Function_Abs__". -inline cic:/CoRN/reals/Max_AbsIR/Q.con. +inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/Q.con" "Part_Function_Abs__". (* end hide *) -inline cic:/CoRN/reals/Max_AbsIR/FMin.con. +inline "cic:/CoRN/reals/Max_AbsIR/FMin.con". -inline cic:/CoRN/reals/Max_AbsIR/FAbs.con. +inline "cic:/CoRN/reals/Max_AbsIR/FAbs.con". (* UNEXPORTED Opaque Max. *) -inline cic:/CoRN/reals/Max_AbsIR/FMin_char.con. +inline "cic:/CoRN/reals/Max_AbsIR/FMin_char.con". (* UNEXPORTED Transparent Max. *) -inline cic:/CoRN/reals/Max_AbsIR/FAbs_char.con. +inline "cic:/CoRN/reals/Max_AbsIR/FAbs_char.con". (* UNEXPORTED -End Part_Function_Abs. +End Part_Function_Abs *) (* UNEXPORTED Hint Resolve FAbs_char: algebra. *) -inline cic:/CoRN/reals/Max_AbsIR/FAbs_char'.con. +inline "cic:/CoRN/reals/Max_AbsIR/FAbs_char'.con". -inline cic:/CoRN/reals/Max_AbsIR/FAbs_nonneg.con. +inline "cic:/CoRN/reals/Max_AbsIR/FAbs_nonneg.con". (* UNEXPORTED Hint Resolve FAbs_char': algebra. *) (* UNEXPORTED -Section Inclusion. +Section Inclusion *) -inline cic:/CoRN/reals/Max_AbsIR/F.var. +inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/F.var" "Inclusion__". -inline cic:/CoRN/reals/Max_AbsIR/G.var. +inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/G.var" "Inclusion__". (* begin hide *) -inline cic:/CoRN/reals/Max_AbsIR/P.con. +inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/P.con" "Inclusion__". -inline cic:/CoRN/reals/Max_AbsIR/Q.con. +inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/Q.con" "Inclusion__". (* end hide *) @@ -380,26 +380,26 @@ inline cic:/CoRN/reals/Max_AbsIR/Q.con. %\end{convention}% *) -inline cic:/CoRN/reals/Max_AbsIR/R.var. +inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/R.var" "Inclusion__". -inline cic:/CoRN/reals/Max_AbsIR/included_FMax.con. +inline "cic:/CoRN/reals/Max_AbsIR/included_FMax.con". -inline cic:/CoRN/reals/Max_AbsIR/included_FMax'.con. +inline "cic:/CoRN/reals/Max_AbsIR/included_FMax'.con". -inline cic:/CoRN/reals/Max_AbsIR/included_FMax''.con. +inline "cic:/CoRN/reals/Max_AbsIR/included_FMax''.con". -inline cic:/CoRN/reals/Max_AbsIR/included_FMin.con. +inline "cic:/CoRN/reals/Max_AbsIR/included_FMin.con". -inline cic:/CoRN/reals/Max_AbsIR/included_FMin'.con. +inline "cic:/CoRN/reals/Max_AbsIR/included_FMin'.con". -inline cic:/CoRN/reals/Max_AbsIR/included_FMin''.con. +inline "cic:/CoRN/reals/Max_AbsIR/included_FMin''.con". -inline cic:/CoRN/reals/Max_AbsIR/included_FAbs.con. +inline "cic:/CoRN/reals/Max_AbsIR/included_FAbs.con". -inline cic:/CoRN/reals/Max_AbsIR/included_FAbs'.con. +inline "cic:/CoRN/reals/Max_AbsIR/included_FAbs'.con". (* UNEXPORTED -End Inclusion. +End Inclusion *) (* UNEXPORTED