helm/software/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 (* $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
  26 CauchySeq
  27 *)
  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 inline cic:/CoRN/reals/Max_AbsIR/x.var.
  46
  47 inline cic:/CoRN/reals/Max_AbsIR/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 inline cic:/CoRN/reals/Max_AbsIR/a.var.
 182
 183 inline cic:/CoRN/reals/Max_AbsIR/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 inline cic:/CoRN/reals/Max_AbsIR/F.var.
 295
 296 inline cic:/CoRN/reals/Max_AbsIR/G.var.
 297
 298 (* begin hide *)
 299
 300 inline cic:/CoRN/reals/Max_AbsIR/P.con.
 301
 302 inline cic:/CoRN/reals/Max_AbsIR/Q.con.
 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 inline cic:/CoRN/reals/Max_AbsIR/F.var.
 319
 320 inline cic:/CoRN/reals/Max_AbsIR/G.var.
 321
 322 (* begin hide *)
 323
 324 inline cic:/CoRN/reals/Max_AbsIR/P.con.
 325
 326 inline cic:/CoRN/reals/Max_AbsIR/Q.con.
 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 inline cic:/CoRN/reals/Max_AbsIR/F.var.
 367
 368 inline cic:/CoRN/reals/Max_AbsIR/G.var.
 369
 370 (* begin hide *)
 371
 372 inline cic:/CoRN/reals/Max_AbsIR/P.con.
 373
 374 inline cic:/CoRN/reals/Max_AbsIR/Q.con.
 375
 376 (* end hide *)
 377
 378 (*#*
 379 %\begin{convention}% Let [R:IR->CProp].
 380 %\end{convention}%
 381 *)
 382
 383 inline cic:/CoRN/reals/Max_AbsIR/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