matita/contribs/CoRN-Decl/CoRN.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/CoRN".
  18
  19 (* From algebra/Basics ****************************************************)
  20
  21 (* NOTATION
  22 Notation Pair := (pair (B:=_)).
  23 *)
  24
  25 (* NOTATION
  26 Notation Proj1 := (proj1 (B:=_)).
  27 *)
  28
  29 (* NOTATION
  30 Notation Proj2 := (proj2 (B:=_)).
  31 *)
  32
  33 (* From algebra/CFields ***************************************************)
  34
  35 (* NOTATION
  36 Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
  37 *)
  38
  39 (* NOTATION
  40 Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
  41 *)
  42
  43 (* NOTATION
  44 Infix "{/}" := Fdiv (at level 41, no associativity).
  45 *)
  46
  47 (* From algebra/CGroups ***************************************************)
  48
  49 (* NOTATION
  50 Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
  51 *)
  52
  53 (* NOTATION
  54 Infix "[-]" := cg_minus (at level 50, left associativity).
  55 *)
  56
  57 (* NOTATION
  58 Notation "{--} x" := (Finv x) (at level 2, right associativity).
  59 *)
  60
  61 (* NOTATION
  62 Infix "{-}" := Fminus (at level 50, left associativity).
  63 *)
  64
  65 (* From algebra/CLogic ****************************************************)
  66
  67 (* NOTATION
  68 Infix "IFF" := Iff (at level 60, right associativity).
  69 *)
  70
  71 (* NOTATION
  72 Infix "or" := COr (at level 85, right associativity).
  73 *)
  74
  75 (* NOTATION
  76 Infix "and" := CAnd (at level 80, right associativity).
  77 *)
  78
  79 (* NOTATION
  80 Notation "{ x : A  |  P }" := (sigT (fun x : A => P):CProp)
  81   (at level 0, x at level 99) : type_scope.
  82 *)
  83
  84 (* NOTATION
  85 Notation "{ x : A  |  P  |  Q }" :=
  86   (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
  87   type_scope.
  88 *)
  89
  90 (* NOTATION
  91 Notation ProjT1 := (proj1_sigT _ _).
  92 *)
  93
  94 (* NOTATION
  95 Notation ProjT2 := (proj2_sigT _ _).
  96 *)
  97
  98 (* From algebra/CMonoids **************************************************)
  99
 100 (* NOTATION
 101 Notation Zero := (cm_unit _).
 102 *)
 103
 104 (* From algebra/COrdAbs ***************************************************)
 105
 106 (* NOTATION
 107 Notation ZeroR := (Zero:R).
 108 *)
 109
 110 (* NOTATION
 111 Notation AbsBig := (absBig _).
 112 *)
 113
 114 (* From algebra/COrdFields ************************************************)
 115
 116 (* NOTATION
 117 Infix "[<]" := cof_less (at level 70, no associativity).
 118 *)
 119
 120 (* NOTATION
 121 Infix "[>]" := greater (at level 70, no associativity).
 122 *)
 123
 124 (* NOTATION
 125 Infix "[<=]" := leEq (at level 70, no associativity).
 126 *)
 127
 128 (* NOTATION
 129 Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
 130 *)
 131
 132 (* NOTATION
 133 Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
 134 *)
 135
 136 (* NOTATION
 137 Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
 138 *)
 139
 140 (* NOTATION
 141 Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
 142 *)
 143
 144 (* NOTATION
 145 Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
 146 *)
 147
 148 (* NOTATION
 149 Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
 150 *)
 151
 152 (* NOTATION
 153 Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
 154 *)
 155
 156 (* NOTATION
 157 Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
 158 *)
 159
 160 (* NOTATION
 161 Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
 162 *)
 163
 164 (* NOTATION
 165 Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
 166 *)
 167
 168 (* NOTATION
 169 Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
 170 *)
 171
 172 (* NOTATION
 173 Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
 174 *)
 175
 176 (* From algebra/COrdFields2 ***********************************************)
 177
 178 (* NOTATION
 179 Notation ZeroR := (Zero:R).
 180 *)
 181
 182 (* NOTATION
 183 Notation OneR := (One:R).
 184 *)
 185
 186 (* From algebra/CPoly_ApZero **********************************************)
 187
 188 (* NOTATION
 189 Notation RX := (cpoly_cring R).
 190 *)
 191
 192 (* NOTATION
 193 Notation RX := (cpoly_cring R).
 194 *)
 195
 196 (* NOTATION
 197 Notation RX := (cpoly_cring R).
 198 *)
 199
 200 (* From algebra/CPoly_Degree **********************************************)
 201
 202 (* NOTATION
 203 Notation RX := (cpoly_cring R).
 204 *)
 205
 206 (* NOTATION
 207 Notation RX := (cpoly_cring R).
 208 *)
 209
 210 (* NOTATION
 211 Notation FX := (cpoly_cring F).
 212 *)
 213
 214 (* From algebra/CPoly_NthCoeff ********************************************)
 215
 216 (* NOTATION
 217 Notation RX := (cpoly_cring R).
 218 *)
 219
 220 (* NOTATION
 221 Notation RX := (cpoly_cring R).
 222 *)
 223
 224 (* From algebra/CPolynomials **********************************************)
 225
 226 (* NOTATION
 227 Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity).
 228 *)
 229
 230 (* NOTATION
 231 Notation RX := (cpoly_cring CR).
 232 *)
 233
 234 (* NOTATION
 235 Infix "!" := cpoly_apply_fun (at level 1, no associativity).
 236 *)
 237
 238 (* NOTATION
 239 Notation RX := (cpoly_cring R).
 240 *)
 241
 242 (* NOTATION
 243 Notation Cpoly := (cpoly CR).
 244 *)
 245
 246 (* NOTATION
 247 Notation Cpoly_zero := (cpoly_zero CR).
 248 *)
 249
 250 (* NOTATION
 251 Notation Cpoly_linear := (cpoly_linear CR).
 252 *)
 253
 254 (* NOTATION
 255 Notation Cpoly_cring := (cpoly_cring CR).
 256 *)
 257
 258 (* From algebra/CRings ****************************************************)
 259
 260 (* NOTATION
 261 Notation One := (cr_one _).
 262 *)
 263
 264 (* NOTATION
 265 Infix "[*]" := cr_mult (at level 40, left associativity).
 266 *)
 267
 268 (* NOTATION
 269 Notation "x [^] n" := (nexp_op _ n x) (at level 20).
 270 *)
 271
 272 (* NOTATION
 273 Notation Two := (nring 2).
 274 *)
 275
 276 (* NOTATION
 277 Notation Three := (nring 3).
 278 *)
 279
 280 (* NOTATION
 281 Notation Four := (nring 4).
 282 *)
 283
 284 (* NOTATION
 285 Notation Six := (nring 6).
 286 *)
 287
 288 (* NOTATION
 289 Notation Eight := (nring 8).
 290 *)
 291
 292 (* NOTATION
 293 Notation Twelve := (nring 12).
 294 *)
 295
 296 (* NOTATION
 297 Notation Sixteen := (nring 16).
 298 *)
 299
 300 (* NOTATION
 301 Notation Nine := (nring 9).
 302 *)
 303
 304 (* NOTATION
 305 Notation Eighteen := (nring 18).
 306 *)
 307
 308 (* NOTATION
 309 Notation TwentyFour := (nring 24).
 310 *)
 311
 312 (* NOTATION
 313 Notation FortyEight := (nring 48).
 314 *)
 315
 316 (* NOTATION
 317 Infix "{*}" := Fmult (at level 40, left associativity).
 318 *)
 319
 320 (* NOTATION
 321 Infix "{**}" := Fscalmult (at level 40, left associativity).
 322 *)
 323
 324 (* NOTATION
 325 Infix "{^}" := Fnth (at level 30, right associativity).
 326 *)
 327
 328 (* From algebra/CSemiGroups ***********************************************)
 329
 330 (* NOTATION
 331 Infix "[+]" := csg_op (at level 50, left associativity).
 332 *)
 333
 334 (* NOTATION
 335 Infix "{+}" := Fplus (at level 50, left associativity).
 336 *)
 337
 338 (* From algebra/CSetoidFun ************************************************)
 339
 340 (* NOTATION
 341 Notation Conj := (conjP _).
 342 *)
 343
 344 (* NOTATION
 345 Notation BDom := (bpfdom _ _).
 346 *)
 347
 348 (* NOTATION
 349 Notation Dom := (pfdom _).
 350 *)
 351
 352 (* NOTATION
 353 Notation Part := (pfpfun _).
 354 *)
 355
 356 (* NOTATION
 357 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
 358 *)
 359
 360 (* NOTATION
 361 Notation FId := (Fid _).
 362 *)
 363
 364 (* NOTATION
 365 Infix "[o]" := Fcomp (at level 65, no associativity).
 366 *)
 367
 368 (* NOTATION
 369 Notation Prj1 := (prj1 _ _ _ _).
 370 *)
 371
 372 (* NOTATION
 373 Notation Prj2 := (prj2 _ _ _ _).
 374 *)
 375
 376 (* From algebra/CSetoids **************************************************)
 377
 378 (* NOTATION
 379 Infix "[=]" := cs_eq (at level 70, no associativity).
 380 *)
 381
 382 (* NOTATION
 383 Infix "[#]" := cs_ap (at level 70, no associativity).
 384 *)
 385
 386 (* NOTATION
 387 Infix "[~=]" := cs_neq (at level 70, no associativity).
 388 *)
 389
 390 (* From algebra/CVectorSpace **********************************************)
 391
 392 (* NOTATION
 393 Infix "[']" := vs_op (at level 30, no associativity).
 394 *)
 395
 396 (* From algebra/Expon *****************************************************)
 397
 398 (* NOTATION
 399 Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0).
 400 *)
 401
 402 (* From complex/CComplex **************************************************)
 403
 404 (* NOTATION
 405 Notation CCX := (cpoly_cring CC).
 406 *)
 407
 408 (* NOTATION
 409 Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
 410 *)
 411
 412 (* From ftc/FTC ***********************************************************)
 413
 414 (* NOTATION
 415 Notation "[-S-] F" := (Fprim F) (at level 20).
 416 *)
 417
 418 (* From ftc/Integral ******************************************************)
 419
 420 (* NOTATION
 421 Notation Integral := (integral _ _ Hab).
 422 *)
 423
 424 (* From ftc/RefLemma ******************************************************)
 425
 426 (* NOTATION
 427 Notation g := RL_g.
 428 *)
 429
 430 (* NOTATION
 431 Notation h := RL_h.
 432 *)
 433
 434 (* NOTATION
 435 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
 436 *)
 437
 438 (* NOTATION
 439 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
 440 *)
 441
 442 (* NOTATION
 443 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
 444 *)
 445
 446 (* From ftc/RefSeparated **************************************************)
 447
 448 (* NOTATION
 449 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
 450 *)
 451
 452 (* NOTATION
 453 Notation just2 :=
 454   (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)).
 455 *)
 456
 457 (* From ftc/RefSeparating *************************************************)
 458
 459 (* NOTATION
 460 Notation m := RS'_m.
 461 *)
 462
 463 (* NOTATION
 464 Notation h := RS'_h.
 465 *)
 466
 467 (* NOTATION
 468 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
 469 *)
 470
 471 (* NOTATION
 472 Notation just2 :=
 473   (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)).
 474 *)
 475
 476 (* From ftc/Rolle *********************************************************)
 477
 478 (* NOTATION
 479 Notation cp := (compact_part a b Hab' d Hd).
 480 *)
 481
 482 (* From ftc/TaylorLemma ***************************************************)
 483
 484 (* NOTATION
 485 Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
 486 *)
 487
 488 (* NOTATION
 489 Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
 490 *)
 491
 492 (* From ftc/WeakIVT *******************************************************)
 493
 494 (* NOTATION
 495 Infix "**" := prodT (at level 20).
 496 *)
 497
 498 (* From metrics/CPseudoMSpaces ********************************************)
 499
 500 (* NOTATION
 501 Infix "[-d]" := cms_d (at level 68, left associativity).
 502 *)
 503
 504 (* From model/structures/Nsec *********************************************)
 505
 506 (* NOTATION
 507 Infix "{#N}" := ap_nat (no associativity, at level 90).
 508 *)
 509
 510 (* From model/structures/Qsec *********************************************)
 511
 512 (* NOTATION
 513 Infix "{=Q}" := Qeq (no associativity, at level 90).
 514 *)
 515
 516 (* NOTATION
 517 Infix "{#Q}" := Qap (no associativity, at level 90).
 518 *)
 519
 520 (* NOTATION
 521 Infix "{<Q}" := Qlt (no associativity, at level 90).
 522 *)
 523
 524 (* NOTATION
 525 Infix "{+Q}" := Qplus (no associativity, at level 85).
 526 *)
 527
 528 (* NOTATION
 529 Infix "{*Q}" := Qmult (no associativity, at level 80).
 530 *)
 531
 532 (* NOTATION
 533 Notation "{-Q}" := Qopp (at level 1, left associativity).
 534 *)
 535
 536 (* From model/structures/Zsec *********************************************)
 537
 538 (* NOTATION
 539 Infix "{#Z}" := ap_Z (no associativity, at level 90).
 540 *)
 541
 542 (* From reals/Bridges_LUB *************************************************)
 543
 544 (* NOTATION
 545 Notation "( p , q )" := (pairT p q).
 546 *)
 547
 548 (* From reals/CMetricFields ***********************************************)
 549
 550 (* NOTATION
 551 Notation MAbs := (cmf_abs _).
 552 *)
 553
 554 (* From reals/CauchySeq ***************************************************)
 555
 556 (* NOTATION
 557 Notation PartIR := (PartFunct IR).
 558 *)
 559
 560 (* NOTATION
 561 Notation ProjIR1 := (prj1 IR _ _ _).
 562 *)
 563
 564 (* NOTATION
 565 Notation ProjIR2 := (prj2 IR _ _ _).
 566 *)
 567
 568 (* NOTATION
 569 Notation ZeroR := (Zero:IR).
 570 *)
 571
 572 (* NOTATION
 573 Notation OneR := (One:IR).
 574 *)
 575
 576 (* From reals/Cauchy_CReals ***********************************************)
 577
 578 (* NOTATION
 579 Notation "'R_COrdField''" := (R_COrdField F).
 580 *)
 581
 582 (* From reals/Intervals ***************************************************)
 583
 584 (* NOTATION
 585 Notation Compact := (compact _ _).
 586 *)
 587
 588 (* NOTATION
 589 Notation FRestr := (Frestr (compact_wd _ _ _)).
 590 *)
 591
 592 (* From reals/Q_dense *****************************************************)
 593
 594 (* NOTATION
 595 Notation "( A , B )" := (pairT A B).
 596 *)
 597
 598 (* From tactics/FieldReflection *******************************************)
 599
 600 (* NOTATION
 601 Notation II := (interpF F val unop binop pfun).
 602 *)
 603
 604 (* From tactics/GroupReflection *******************************************)
 605
 606 (* NOTATION
 607 Notation II := (interpG G val unop binop pfun).
 608 *)
 609
 610 (* From tactics/RingReflection ********************************************)
 611
 612 (* NOTATION
 613 Notation II := (interpR R val unop binop pfun).
 614 *)
 615
 616 (* From transc/RealPowers *************************************************)
 617
 618 (* NOTATION
 619 Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
 620 *)
 621
 622 (* NOTATION
 623 Notation "F {!} G" := (FPower F G) (at level 20).
 624 *)
 625