helm/software/matita/contribs/procedural/CoRN/reals/Max_AbsIR.mma

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