1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/CoRN".
19 (* From algebra/Basics ****************************************************)
22 Notation Pair := (pair (B:=_)).
26 Notation Proj1 := (proj1 (B:=_)).
30 Notation Proj2 := (proj2 (B:=_)).
33 (* From algebra/CFields ***************************************************)
36 Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
40 Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
44 Infix "{/}" := Fdiv (at level 41, no associativity).
47 (* From algebra/CGroups ***************************************************)
50 Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
54 Infix "[-]" := cg_minus (at level 50, left associativity).
58 Notation "{--} x" := (Finv x) (at level 2, right associativity).
62 Infix "{-}" := Fminus (at level 50, left associativity).
65 (* From algebra/CLogic ****************************************************)
68 Infix "IFF" := Iff (at level 60, right associativity).
72 Infix "or" := COr (at level 85, right associativity).
76 Infix "and" := CAnd (at level 80, right associativity).
80 Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp)
81 (at level 0, x at level 99) : type_scope.
85 Notation "{ x : A | P | Q }" :=
86 (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) :
91 Notation ProjT1 := (proj1_sigT _ _).
95 Notation ProjT2 := (proj2_sigT _ _).
98 (* From algebra/CMonoids **************************************************)
101 Notation Zero := (cm_unit _).
104 (* From algebra/COrdAbs ***************************************************)
107 Notation ZeroR := (Zero:R).
111 Notation AbsBig := (absBig _).
114 (* From algebra/COrdFields ************************************************)
117 Infix "[<]" := cof_less (at level 70, no associativity).
121 Infix "[>]" := greater (at level 70, no associativity).
125 Infix "[<=]" := leEq (at level 70, no associativity).
129 Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20).
133 Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20).
137 Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20).
141 Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20).
145 Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20).
149 Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20).
153 Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20).
157 Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20).
161 Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20).
165 Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20).
169 Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20).
173 Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20).
176 (* From algebra/COrdFields2 ***********************************************)
179 Notation ZeroR := (Zero:R).
183 Notation OneR := (One:R).
186 (* From algebra/CPoly_ApZero **********************************************)
189 Notation RX := (cpoly_cring R).
193 Notation RX := (cpoly_cring R).
197 Notation RX := (cpoly_cring R).
200 (* From algebra/CPoly_Degree **********************************************)
203 Notation RX := (cpoly_cring R).
207 Notation RX := (cpoly_cring R).
211 Notation FX := (cpoly_cring F).
214 (* From algebra/CPoly_NthCoeff ********************************************)
217 Notation RX := (cpoly_cring R).
221 Notation RX := (cpoly_cring R).
224 (* From algebra/CPolynomials **********************************************)
227 Infix "[+X*]" := cpoly_linear_fun' (at level 50, left associativity).
231 Notation RX := (cpoly_cring CR).
235 Infix "!" := cpoly_apply_fun (at level 1, no associativity).
239 Notation RX := (cpoly_cring R).
243 Notation Cpoly := (cpoly CR).
247 Notation Cpoly_zero := (cpoly_zero CR).
251 Notation Cpoly_linear := (cpoly_linear CR).
255 Notation Cpoly_cring := (cpoly_cring CR).
258 (* From algebra/CRings ****************************************************)
261 Notation One := (cr_one _).
265 Infix "[*]" := cr_mult (at level 40, left associativity).
269 Notation "x [^] n" := (nexp_op _ n x) (at level 20).
273 Notation Two := (nring 2).
277 Notation Three := (nring 3).
281 Notation Four := (nring 4).
285 Notation Six := (nring 6).
289 Notation Eight := (nring 8).
293 Notation Twelve := (nring 12).
297 Notation Sixteen := (nring 16).
301 Notation Nine := (nring 9).
305 Notation Eighteen := (nring 18).
309 Notation TwentyFour := (nring 24).
313 Notation FortyEight := (nring 48).
317 Infix "{*}" := Fmult (at level 40, left associativity).
321 Infix "{**}" := Fscalmult (at level 40, left associativity).
325 Infix "{^}" := Fnth (at level 30, right associativity).
328 (* From algebra/CSemiGroups ***********************************************)
331 Infix "[+]" := csg_op (at level 50, left associativity).
335 Infix "{+}" := Fplus (at level 50, left associativity).
338 (* From algebra/CSetoidFun ************************************************)
341 Notation Conj := (conjP _).
345 Notation BDom := (bpfdom _ _).
349 Notation Dom := (pfdom _).
353 Notation Part := (pfpfun _).
357 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
361 Notation FId := (Fid _).
365 Infix "[o]" := Fcomp (at level 65, no associativity).
369 Notation Prj1 := (prj1 _ _ _ _).
373 Notation Prj2 := (prj2 _ _ _ _).
376 (* From algebra/CSetoids **************************************************)
379 Infix "[=]" := cs_eq (at level 70, no associativity).
383 Infix "[#]" := cs_ap (at level 70, no associativity).
387 Infix "[~=]" := cs_neq (at level 70, no associativity).
390 (* From algebra/CVectorSpace **********************************************)
393 Infix "[']" := vs_op (at level 30, no associativity).
396 (* From algebra/Expon *****************************************************)
399 Notation "( x [//] Hx ) [^^] n" := (zexp x Hx n) (at level 0).
402 (* From complex/CComplex **************************************************)
405 Notation CCX := (cpoly_cring CC).
409 Infix "[+I*]" := cc_set_CC (at level 48, no associativity).
412 (* From ftc/FTC ***********************************************************)
415 Notation "[-S-] F" := (Fprim F) (at level 20).
418 (* From ftc/Integral ******************************************************)
421 Notation Integral := (integral _ _ Hab).
424 (* From ftc/RefLemma ******************************************************)
435 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
439 Notation just2 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfQ _ _)).
443 Notation just := (fun z => incF _ (Pts_part_lemma _ _ _ _ _ _ z _ _)).
446 (* From ftc/RefSeparated **************************************************)
449 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
454 (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__sep_points_lemma _ _)).
457 (* From ftc/RefSeparating *************************************************)
468 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ gP _ _)).
473 (incF _ (Pts_part_lemma _ _ _ _ _ _ sep__part_pts_in_Partition _ _)).
476 (* From ftc/Rolle *********************************************************)
479 Notation cp := (compact_part a b Hab' d Hd).
482 (* From ftc/TaylorLemma ***************************************************)
485 Notation A := (Build_subcsetoid_crr IR _ _ TL_compact_a).
489 Notation B := (Build_subcsetoid_crr IR _ _ TL_compact_b).
492 (* From ftc/WeakIVT *******************************************************)
495 Infix "**" := prodT (at level 20).
498 (* From metrics/CPseudoMSpaces ********************************************)
501 Infix "[-d]" := cms_d (at level 68, left associativity).
504 (* From model/structures/Nsec *********************************************)
507 Infix "{#N}" := ap_nat (no associativity, at level 90).
510 (* From model/structures/Qsec *********************************************)
513 Infix "{=Q}" := Qeq (no associativity, at level 90).
517 Infix "{#Q}" := Qap (no associativity, at level 90).
521 Infix "{<Q}" := Qlt (no associativity, at level 90).
525 Infix "{+Q}" := Qplus (no associativity, at level 85).
529 Infix "{*Q}" := Qmult (no associativity, at level 80).
533 Notation "{-Q}" := Qopp (at level 1, left associativity).
536 (* From model/structures/Zsec *********************************************)
539 Infix "{#Z}" := ap_Z (no associativity, at level 90).
542 (* From reals/Bridges_LUB *************************************************)
545 Notation "( p , q )" := (pairT p q).
548 (* From reals/CMetricFields ***********************************************)
551 Notation MAbs := (cmf_abs _).
554 (* From reals/CauchySeq ***************************************************)
557 Notation PartIR := (PartFunct IR).
561 Notation ProjIR1 := (prj1 IR _ _ _).
565 Notation ProjIR2 := (prj2 IR _ _ _).
569 Notation ZeroR := (Zero:IR).
573 Notation OneR := (One:IR).
576 (* From reals/Cauchy_CReals ***********************************************)
579 Notation "'R_COrdField''" := (R_COrdField F).
582 (* From reals/Intervals ***************************************************)
585 Notation Compact := (compact _ _).
589 Notation FRestr := (Frestr (compact_wd _ _ _)).
592 (* From reals/Q_dense *****************************************************)
595 Notation "( A , B )" := (pairT A B).
598 (* From tactics/FieldReflection *******************************************)
601 Notation II := (interpF F val unop binop pfun).
604 (* From tactics/GroupReflection *******************************************)
607 Notation II := (interpG G val unop binop pfun).
610 (* From tactics/RingReflection ********************************************)
613 Notation II := (interpR R val unop binop pfun).
616 (* From transc/RealPowers *************************************************)
619 Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
623 Notation "F {!} G" := (FPower F G) (at level 20).