matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/reals/Max_AbsIR".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: Max_AbsIR.v,v 1.13 2004/04/23 10:01:04 lcf Exp $ *)
  22
  23 (*#* printing Max %\ensuremath{\max}% *)
  24
  25 (*#* printing Min %\ensuremath{\min}% *)
  26
  27 include "reals/CauchySeq.ma".
  28
  29 (* UNEXPORTED
  30 Section Maximum
  31 *)
  32
  33 (* UNEXPORTED
  34 Section Max_function
  35 *)
  36
  37 (*#* ** Maximum, Minimum and Absolute Value
  38
  39 %\begin{convention}%
  40 Let [x] and [y] be reals
  41 (we will define the maximum of [x] and [y]).
  42 %\end{convention}%
  43 *)
  44
  45 alias id "x" = "cic:/CoRN/reals/Max_AbsIR/Maximum/Max_function/x.var".
  46
  47 alias id "y" = "cic:/CoRN/reals/Max_AbsIR/Maximum/Max_function/y.var".
  48
  49 inline "cic:/CoRN/reals/Max_AbsIR/Max_seq.con".
  50
  51 inline "cic:/CoRN/reals/Max_AbsIR/Max_seq_char.con".
  52
  53 inline "cic:/CoRN/reals/Max_AbsIR/Cauchy_Max_seq.con".
  54
  55 inline "cic:/CoRN/reals/Max_AbsIR/Max_CauchySeq.con".
  56
  57 inline "cic:/CoRN/reals/Max_AbsIR/MAX.con".
  58
  59 (*#*
  60 Constructively, the elementary properties of the maximum function are:
  61 - [x [<=] Max (x,y)],
  62 - [x [<=] Max (y,x)],
  63 - [z [<] Max(x,y) -> z [<] x or z [<] y].
  64
  65 (This can be more concisely expressed as
  66 [z [<] Max(x,y) Iff z [<] x or z [<] y]).
  67 From these elementary properties we can prove all other properties, including
  68 strong extensionality.
  69 With strong extensionality, we can make the binary operation [Max].
  70 (So [Max] is [MAX] coupled with some proofs.)
  71 *)
  72
  73 inline "cic:/CoRN/reals/Max_AbsIR/lft_leEq_MAX.con".
  74
  75 inline "cic:/CoRN/reals/Max_AbsIR/rht_leEq_MAX.con".
  76
  77 inline "cic:/CoRN/reals/Max_AbsIR/less_MAX_imp.con".
  78
  79 (* UNEXPORTED
  80 End Max_function
  81 *)
  82
  83 inline "cic:/CoRN/reals/Max_AbsIR/MAX_strext.con".
  84
  85 inline "cic:/CoRN/reals/Max_AbsIR/MAX_wd.con".
  86
  87 (* UNEXPORTED
  88 Section properties_of_Max
  89 *)
  90
  91 (*#* *** Maximum *)
  92
  93 inline "cic:/CoRN/reals/Max_AbsIR/Max.con".
  94
  95 inline "cic:/CoRN/reals/Max_AbsIR/Max_wd_unfolded.con".
  96
  97 inline "cic:/CoRN/reals/Max_AbsIR/lft_leEq_Max.con".
  98
  99 inline "cic:/CoRN/reals/Max_AbsIR/rht_leEq_Max.con".
 100
 101 inline "cic:/CoRN/reals/Max_AbsIR/less_Max_imp.con".
 102
 103 inline "cic:/CoRN/reals/Max_AbsIR/Max_leEq.con".
 104
 105 inline "cic:/CoRN/reals/Max_AbsIR/Max_less.con".
 106
 107 inline "cic:/CoRN/reals/Max_AbsIR/equiv_imp_eq_max.con".
 108
 109 inline "cic:/CoRN/reals/Max_AbsIR/Max_id.con".
 110
 111 inline "cic:/CoRN/reals/Max_AbsIR/Max_comm.con".
 112
 113 inline "cic:/CoRN/reals/Max_AbsIR/leEq_imp_Max_is_rht.con".
 114
 115 inline "cic:/CoRN/reals/Max_AbsIR/Max_is_rht_imp_leEq.con".
 116
 117 inline "cic:/CoRN/reals/Max_AbsIR/Max_minus_eps_leEq.con".
 118
 119 inline "cic:/CoRN/reals/Max_AbsIR/max_one_ap_zero.con".
 120
 121 inline "cic:/CoRN/reals/Max_AbsIR/pos_max_one.con".
 122
 123 inline "cic:/CoRN/reals/Max_AbsIR/x_div_Max_leEq_x.con".
 124
 125 (* UNEXPORTED
 126 End properties_of_Max
 127 *)
 128
 129 (* UNEXPORTED
 130 End Maximum
 131 *)
 132
 133 (* UNEXPORTED
 134 Hint Resolve Max_id: algebra.
 135 *)
 136
 137 (* UNEXPORTED
 138 Section Minimum
 139 *)
 140
 141 (*#* *** Mininum
 142
 143 The minimum is defined by the formula
 144 [Min(x,y) [=] [--]Max( [--]x,[--]y)].
 145 *)
 146
 147 inline "cic:/CoRN/reals/Max_AbsIR/MIN.con".
 148
 149 inline "cic:/CoRN/reals/Max_AbsIR/MIN_wd.con".
 150
 151 inline "cic:/CoRN/reals/Max_AbsIR/MIN_strext.con".
 152
 153 inline "cic:/CoRN/reals/Max_AbsIR/Min.con".
 154
 155 inline "cic:/CoRN/reals/Max_AbsIR/Min_wd_unfolded.con".
 156
 157 inline "cic:/CoRN/reals/Max_AbsIR/Min_strext_unfolded.con".
 158
 159 inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_lft.con".
 160
 161 inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_rht.con".
 162
 163 inline "cic:/CoRN/reals/Max_AbsIR/Min_less_imp.con".
 164
 165 inline "cic:/CoRN/reals/Max_AbsIR/leEq_Min.con".
 166
 167 inline "cic:/CoRN/reals/Max_AbsIR/less_Min.con".
 168
 169 inline "cic:/CoRN/reals/Max_AbsIR/equiv_imp_eq_min.con".
 170
 171 inline "cic:/CoRN/reals/Max_AbsIR/Min_id.con".
 172
 173 inline "cic:/CoRN/reals/Max_AbsIR/Min_comm.con".
 174
 175 inline "cic:/CoRN/reals/Max_AbsIR/leEq_imp_Min_is_lft.con".
 176
 177 inline "cic:/CoRN/reals/Max_AbsIR/Min_is_lft_imp_leEq.con".
 178
 179 inline "cic:/CoRN/reals/Max_AbsIR/leEq_Min_plus_eps.con".
 180
 181 alias id "a" = "cic:/CoRN/reals/Max_AbsIR/Minimum/a.var".
 182
 183 alias id "b" = "cic:/CoRN/reals/Max_AbsIR/Minimum/b.var".
 184
 185 inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max.con".
 186
 187 inline "cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max'.con".
 188
 189 inline "cic:/CoRN/reals/Max_AbsIR/Min3_leEq_Max3.con".
 190
 191 inline "cic:/CoRN/reals/Max_AbsIR/Min_less_Max.con".
 192
 193 inline "cic:/CoRN/reals/Max_AbsIR/ap_imp_Min_less_Max.con".
 194
 195 inline "cic:/CoRN/reals/Max_AbsIR/Min_less_Max_imp_ap.con".
 196
 197 (* UNEXPORTED
 198 End Minimum
 199 *)
 200
 201 (*#**********************************)
 202
 203 (* UNEXPORTED
 204 Section Absolute
 205 *)
 206
 207 (*#**********************************)
 208
 209 (*#* *** Absolute value *)
 210
 211 inline "cic:/CoRN/reals/Max_AbsIR/ABSIR.con".
 212
 213 inline "cic:/CoRN/reals/Max_AbsIR/ABSIR_strext.con".
 214
 215 inline "cic:/CoRN/reals/Max_AbsIR/ABSIR_wd.con".
 216
 217 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR.con".
 218
 219 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_wd.con".
 220
 221 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_wdl.con".
 222
 223 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_wdr.con".
 224
 225 inline "cic:/CoRN/reals/Max_AbsIR/AbsIRz_isz.con".
 226
 227 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_nonneg.con".
 228
 229 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_pos.con".
 230
 231 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_cancel_ap_zero.con".
 232
 233 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_resp_ap_zero.con".
 234
 235 inline "cic:/CoRN/reals/Max_AbsIR/leEq_AbsIR.con".
 236
 237 inline "cic:/CoRN/reals/Max_AbsIR/inv_leEq_AbsIR.con".
 238
 239 inline "cic:/CoRN/reals/Max_AbsIR/AbsSmall_e.con".
 240
 241 inline "cic:/CoRN/reals/Max_AbsIR/AbsSmall_imp_AbsIR.con".
 242
 243 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_AbsSmall.con".
 244
 245 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_imp_AbsSmall.con".
 246
 247 inline "cic:/CoRN/reals/Max_AbsIR/AbsSmall_transitive.con".
 248
 249 inline "cic:/CoRN/reals/Max_AbsIR/zero_less_AbsIR_plus_one.con".
 250
 251 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_inv.con".
 252
 253 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_minus.con".
 254
 255 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_x.con".
 256
 257 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_inv_x.con".
 258
 259 inline "cic:/CoRN/reals/Max_AbsIR/less_AbsIR.con".
 260
 261 inline "cic:/CoRN/reals/Max_AbsIR/leEq_distr_AbsIR.con".
 262
 263 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_approach_zero.con".
 264
 265 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_zero.con".
 266
 267 inline "cic:/CoRN/reals/Max_AbsIR/Abs_Max.con".
 268
 269 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_str_bnd.con".
 270
 271 inline "cic:/CoRN/reals/Max_AbsIR/AbsIR_bnd.con".
 272
 273 (* UNEXPORTED
 274 End Absolute
 275 *)
 276
 277 (* UNEXPORTED
 278 Hint Resolve AbsIRz_isz: algebra.
 279 *)
 280
 281 (* UNEXPORTED
 282 Section Part_Function_Max
 283 *)
 284
 285 (*#* *** Functional Operators
 286
 287 The existence of these operators allows us to lift them to functions.  We will define the maximum, minimum and absolute value of two partial functions.
 288
 289 %\begin{convention}%
 290 Let [F,G:PartIR] and denote by [P] and [Q] their respective domains.
 291 %\end{convention}%
 292 *)
 293
 294 alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/F.var".
 295
 296 alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/G.var".
 297
 298 (* begin hide *)
 299
 300 inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/P.con" "Part_Function_Max__".
 301
 302 inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/Q.con" "Part_Function_Max__".
 303
 304 (* end hide *)
 305
 306 inline "cic:/CoRN/reals/Max_AbsIR/part_function_Max_strext.con".
 307
 308 inline "cic:/CoRN/reals/Max_AbsIR/FMax.con".
 309
 310 (* UNEXPORTED
 311 End Part_Function_Max
 312 *)
 313
 314 (* UNEXPORTED
 315 Section Part_Function_Abs
 316 *)
 317
 318 alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/F.var".
 319
 320 alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/G.var".
 321
 322 (* begin hide *)
 323
 324 inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/P.con" "Part_Function_Abs__".
 325
 326 inline "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/Q.con" "Part_Function_Abs__".
 327
 328 (* end hide *)
 329
 330 inline "cic:/CoRN/reals/Max_AbsIR/FMin.con".
 331
 332 inline "cic:/CoRN/reals/Max_AbsIR/FAbs.con".
 333
 334 (* UNEXPORTED
 335 Opaque Max.
 336 *)
 337
 338 inline "cic:/CoRN/reals/Max_AbsIR/FMin_char.con".
 339
 340 (* UNEXPORTED
 341 Transparent Max.
 342 *)
 343
 344 inline "cic:/CoRN/reals/Max_AbsIR/FAbs_char.con".
 345
 346 (* UNEXPORTED
 347 End Part_Function_Abs
 348 *)
 349
 350 (* UNEXPORTED
 351 Hint Resolve FAbs_char: algebra.
 352 *)
 353
 354 inline "cic:/CoRN/reals/Max_AbsIR/FAbs_char'.con".
 355
 356 inline "cic:/CoRN/reals/Max_AbsIR/FAbs_nonneg.con".
 357
 358 (* UNEXPORTED
 359 Hint Resolve FAbs_char': algebra.
 360 *)
 361
 362 (* UNEXPORTED
 363 Section Inclusion
 364 *)
 365
 366 alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/F.var".
 367
 368 alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/G.var".
 369
 370 (* begin hide *)
 371
 372 inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/P.con" "Inclusion__".
 373
 374 inline "cic:/CoRN/reals/Max_AbsIR/Inclusion/Q.con" "Inclusion__".
 375
 376 (* end hide *)
 377
 378 (*#*
 379 %\begin{convention}% Let [R:IR->CProp].
 380 %\end{convention}%
 381 *)
 382
 383 alias id "R" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/R.var".
 384
 385 inline "cic:/CoRN/reals/Max_AbsIR/included_FMax.con".
 386
 387 inline "cic:/CoRN/reals/Max_AbsIR/included_FMax'.con".
 388
 389 inline "cic:/CoRN/reals/Max_AbsIR/included_FMax''.con".
 390
 391 inline "cic:/CoRN/reals/Max_AbsIR/included_FMin.con".
 392
 393 inline "cic:/CoRN/reals/Max_AbsIR/included_FMin'.con".
 394
 395 inline "cic:/CoRN/reals/Max_AbsIR/included_FMin''.con".
 396
 397 inline "cic:/CoRN/reals/Max_AbsIR/included_FAbs.con".
 398
 399 inline "cic:/CoRN/reals/Max_AbsIR/included_FAbs'.con".
 400
 401 (* UNEXPORTED
 402 End Inclusion
 403 *)
 404
 405 (* UNEXPORTED
 406 Hint Resolve included_FMax included_FMin included_FAbs : included.
 407 *)
 408
 409 (* UNEXPORTED
 410 Hint Immediate included_FMax' included_FMin' included_FAbs'
 411   included_FMax'' included_FMin'' : included.
 412 *)
 413