Bibliographic Cross-References
|
|
Metamath Proof Explorer Bibliographic Cross-References |
|
| Mirrors > Home > MPE Home > Bibliographic Cross-References | ||
| Color key: |
Metamath Proof Explorer |
Hilbert Space Explorer |
 User Mathboxes |
| Bibliographic Reference | Description | Metamath Proof Explorer Page(s) |
|---|---|---|
| [Adamek] p. 21 | Definition 3.1 | df-cat 16536 |
| [Adamek] p. 21 | Condition 3.1(b) | df-cat 16536 |
| [Adamek] p. 22 | Example 3.3(1) | df-setc 16933 |
| [Adamek] p. 24 | Example 3.3(4.c) | 0cat 16556 |
| [Adamek] p. 25 | Definition 3.5 | df-oppc 16579 |
| [Adamek] p. 28 | Remark 3.9 | oppciso 16648 |
| [Adamek] p. 28 | Remark 3.12 | invf1o 16636 invisoinvl 16657 |
| [Adamek] p. 28 | Example 3.13 | idinv 16656 idiso 16655 |
| [Adamek] p. 28 | Corollary 3.11 | inveq 16641 |
| [Adamek] p. 28 | Definition 3.8 | df-inv 16615 df-iso 16616 dfiso2 16639 |
| [Adamek] p. 28 | Proposition 3.10 | sectcan 16622 |
| [Adamek] p. 29 | Remark 3.16 | cicer 16673 |
| [Adamek] p. 29 | Definition 3.15 | cic 16666 df-cic 16663 |
| [Adamek] p. 29 | Definition 3.17 | df-func 16725 |
| [Adamek] p. 29 | Proposition 3.14(1) | invinv 16637 |
| [Adamek] p. 29 | Proposition 3.14(2) | invco 16638 isoco 16644 |
| [Adamek] p. 30 | Remark 3.19 | df-func 16725 |
| [Adamek] p. 30 | Example 3.20(1) | idfucl 16748 |
| [Adamek] p. 32 | Proposition 3.21 | funciso 16741 |
| [Adamek] p. 33 | Proposition 3.23 | cofucl 16755 |
| [Adamek] p. 34 | Remark 3.28(2) | catciso 16964 |
| [Adamek] p. 34 | Remark 3.28 (1) | embedsetcestrc 17015 |
| [Adamek] p. 34 | Definition 3.27(2) | df-fth 16772 |
| [Adamek] p. 34 | Definition 3.27(3) | df-full 16771 |
| [Adamek] p. 34 | Definition 3.27 (1) | embedsetcestrc 17015 |
| [Adamek] p. 35 | Corollary 3.32 | ffthiso 16796 |
| [Adamek] p. 35 | Proposition 3.30(c) | cofth 16802 |
| [Adamek] p. 35 | Proposition 3.30(d) | cofull 16801 |
| [Adamek] p. 36 | Definition 3.33 (1) | equivestrcsetc 17000 |
| [Adamek] p. 36 | Definition 3.33 (2) | equivestrcsetc 17000 |
| [Adamek] p. 39 | Definition 3.41 | funcoppc 16742 |
| [Adamek] p. 39 | Definition 3.44. | df-catc 16952 |
| [Adamek] p. 39 | Proposition 3.43(c) | fthoppc 16790 |
| [Adamek] p. 39 | Proposition 3.43(d) | fulloppc 16789 |
| [Adamek] p. 40 | Remark 3.48 | catccat 16961 |
| [Adamek] p. 40 | Definition 3.47 | df-catc 16952 |
| [Adamek] p. 48 | Example 4.3(1.a) | 0subcat 16705 |
| [Adamek] p. 48 | Example 4.3(1.b) | catsubcat 16706 |
| [Adamek] p. 48 | Definition 4.1(2) | fullsubc 16717 |
| [Adamek] p. 48 | Definition 4.1(a) | df-subc 16679 |
| [Adamek] p. 49 | Remark 4.4(2) | ressffth 16805 |
| [Adamek] p. 83 | Definition 6.1 | df-nat 16810 |
| [Adamek] p. 87 | Remark 6.14(a) | fuccocl 16831 |
| [Adamek] p. 87 | Remark 6.14(b) | fucass 16835 |
| [Adamek] p. 87 | Definition 6.15 | df-fuc 16811 |
| [Adamek] p. 88 | Remark 6.16 | fuccat 16837 |
| [Adamek] p. 101 | Definition 7.1 | df-inito 16848 |
| [Adamek] p. 101 | Example 7.2 (6) | irinitoringc 42592 |
| [Adamek] p. 102 | Definition 7.4 | df-termo 16849 |
| [Adamek] p. 102 | Proposition 7.3 (1) | initoeu1w 16869 |
| [Adamek] p. 102 | Proposition 7.3 (2) | initoeu2 16873 |
| [Adamek] p. 103 | Definition 7.7 | df-zeroo 16850 |
| [Adamek] p. 103 | Example 7.9 (3) | nzerooringczr 42595 |
| [Adamek] p. 103 | Proposition 7.6 | termoeu1w 16876 |
| [Adamek] p. 106 | Definition 7.19 | df-sect 16614 |
| [Adamek] p. 478 | Item Rng | df-ringc 42528 |
| [AhoHopUll] p. 2 | Section 1.1 | df-bigo 42865 |
| [AhoHopUll] p. 12 | Section 1.3 | df-blen 42887 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 13497 df-pfx 41905 df-substr 13499 df-word 13495 lencl 13520 wrd0 13526 |
| [AkhiezerGlazman] p. 39 | Linear operator norm | df-nmo 22732 df-nmoo 27940 |
| [AkhiezerGlazman] p. 64 | Theorem | hmopidmch 29352 hmopidmchi 29350 |
| [AkhiezerGlazman] p. 65 | Theorem 1 | pjcmul1i 29400 pjcmul2i 29401 |
| [AkhiezerGlazman] p. 72 | Theorem | cnvunop 29117 unoplin 29119 |
| [AkhiezerGlazman] p. 72 | Equation 2 | unopadj 29118 unopadj2 29137 |
| [AkhiezerGlazman] p. 73 | Theorem | elunop2 29212 lnopunii 29211 |
| [AkhiezerGlazman] p. 80 | Proposition 1 | adjlnop 29285 |
| [Apostol] p. 18 | Theorem I.1 | addcan 10426 addcan2d 10446 addcan2i 10436 addcand 10445 addcani 10435 |
| [Apostol] p. 18 | Theorem I.2 | negeu 10477 |
| [Apostol] p. 18 | Theorem I.3 | negsub 10535 negsubd 10604 negsubi 10565 |
| [Apostol] p. 18 | Theorem I.4 | negneg 10537 negnegd 10589 negnegi 10557 |
| [Apostol] p. 18 | Theorem I.5 | subdi 10669 subdid 10692 subdii 10685 subdir 10670 subdird 10693 subdiri 10686 |
| [Apostol] p. 18 | Theorem I.6 | mul01 10421 mul01d 10441 mul01i 10432 mul02 10420 mul02d 10440 mul02i 10431 |
| [Apostol] p. 18 | Theorem I.7 | mulcan 10870 mulcan2d 10867 mulcand 10866 mulcani 10872 |
| [Apostol] p. 18 | Theorem I.8 | receu 10878 xreceu 29970 |
| [Apostol] p. 18 | Theorem I.9 | divrec 10907 divrecd 11010 divreci 10976 divreczi 10969 |
| [Apostol] p. 18 | Theorem I.10 | recrec 10928 recreci 10963 |
| [Apostol] p. 18 | Theorem I.11 | mul0or 10873 mul0ord 10883 mul0ori 10881 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 10675 mul2negd 10691 mul2negi 10684 mulneg1 10672 mulneg1d 10689 mulneg1i 10682 |
| [Apostol] p. 18 | Theorem I.13 | divadddiv 10946 divadddivd 11051 divadddivi 10993 |
| [Apostol] p. 18 | Theorem I.14 | divmuldiv 10931 divmuldivd 11048 divmuldivi 10991 rdivmuldivd 30131 |
| [Apostol] p. 18 | Theorem I.15 | divdivdiv 10932 divdivdivd 11054 divdivdivi 10994 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 12057 rpaddcld 12090 rpmulcl 12058 rpmulcld 12091 |
| [Apostol] p. 20 | Axiom 8 | rpneg 12066 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 12068 |
| [Apostol] p. 20 | Theorem I.17 | lttri 10369 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 10826 ltadd1dd 10844 ltadd1i 10788 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 11079 ltmul1a 11078 ltmul1i 11148 ltmul1ii 11158 ltmul2 11080 ltmul2d 12117 ltmul2dd 12131 ltmul2i 11151 |
| [Apostol] p. 20 | Theorem I.20 | msqgt0 10754 msqgt0d 10801 msqgt0i 10771 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 10756 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 10740 lt0neg1d 10803 ltneg 10734 ltnegd 10811 ltnegi 10778 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 10719 lt2addd 10856 lt2addi 10796 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 12036 |
| [Apostol] p. 21 | Exercise 4 | recgt0 11073 recgt0d 11164 recgt0i 11134 recgt0ii 11135 |
| [Apostol] p. 22 | Definition of integers | df-z 11585 |
| [Apostol] p. 22 | Definition of positive integers | dfnn3 11240 |
| [Apostol] p. 22 | Definition of rationals | df-q 11997 |
| [Apostol] p. 24 | Theorem I.26 | supeu 8520 |
| [Apostol] p. 26 | Theorem I.28 | nnunb 11495 |
| [Apostol] p. 26 | Theorem I.29 | arch 11496 |
| [Apostol] p. 28 | Exercise 2 | btwnz 11686 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 11497 |
| [Apostol] p. 28 | Exercise 4 | rebtwnz 11995 |
| [Apostol] p. 28 | Exercise 5 | zbtwnre 11994 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 12235 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 15271 zneo 11667 zneoALTV 42103 |
| [Apostol] p. 29 | Theorem I.35 | msqsqrtd 14387 resqrtth 14204 sqrtth 14312 sqrtthi 14318 sqsqrtd 14386 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 11229 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwo 11961 |
| [Apostol] p. 361 | Remark | crreczi 13196 |
| [Apostol] p. 363 | Remark | absgt0i 14346 |
| [Apostol] p. 363 | Example | abssubd 14400 abssubi 14350 |
| [ApostolNT] p. 7 | Remark | fmtno0 41975 fmtno1 41976 fmtno2 41985 fmtno3 41986 fmtno4 41987 fmtno5fac 42017 fmtnofz04prm 42012 |
| [ApostolNT] p. 7 | Definition | df-fmtno 41963 |
| [ApostolNT] p. 8 | Definition | df-ppi 25047 |
| [ApostolNT] p. 14 | Definition | df-dvds 15190 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 15204 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 15227 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 15223 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 15217 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 15219 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 15205 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 15206 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 15211 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 15242 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 15244 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 15246 |
| [ApostolNT] p. 15 | Definition | df-gcd 15425 dfgcd2 15471 |
| [ApostolNT] p. 16 | Definition | isprm2 15602 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 15574 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 15826 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 15443 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 15472 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 15474 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 15457 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 15449 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 15630 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 15632 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 15839 |
| [ApostolNT] p. 18 | Theorem 1.13 | prmrec 15833 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 15334 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 15508 |
| [ApostolNT] p. 24 | Definition | df-mu 25048 |
| [ApostolNT] p. 25 | Definition | df-phi 15678 |
| [ApostolNT] p. 25 | Theorem 2.1 | musum 25138 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 15702 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 15688 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 15692 |
| [ApostolNT] p. 32 | Definition | df-vma 25045 |
| [ApostolNT] p. 32 | Theorem 2.9 | muinv 25140 |
| [ApostolNT] p. 32 | Theorem 2.10 | vmasum 25162 |
| [ApostolNT] p. 38 | Remark | df-sgm 25049 |
| [ApostolNT] p. 38 | Definition | df-sgm 25049 |
| [ApostolNT] p. 75 | Definition | df-chp 25046 df-cht 25044 |
| [ApostolNT] p. 104 | Definition | congr 15585 |
| [ApostolNT] p. 106 | Remark | dvdsval3 15193 |
| [ApostolNT] p. 106 | Definition | moddvds 15200 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 15278 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 15279 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 12895 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modmul12d 12932 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modexp 13206 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 15222 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 15588 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 15985 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 15590 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 15695 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 15713 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 15696 |
| [ApostolNT] p. 116 | Theorem 5.24 | wilthimp 25019 |
| [ApostolNT] p. 179 | Definition | df-lgs 25241 lgsprme0 25285 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 25286 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 25262 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 25277 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 25334 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 25353 2lgsoddprm 25362 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 25320 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 25329 |
| [ApostolNT] p. 188 | Definition | df-lgs 25241 lgs1 25287 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 25278 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 25280 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 25288 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 25289 |
| [Baer] p. 40 | Property (b) | mapdord 37446 |
| [Baer] p. 40 | Property (c) | mapd11 37447 |
| [Baer] p. 40 | Property (e) | mapdin 37470 mapdlsm 37472 |
| [Baer] p. 40 | Property (f) | mapd0 37473 |
| [Baer] p. 40 | Definition of projectivity | df-mapd 37433 mapd1o 37456 |
| [Baer] p. 41 | Property (g) | mapdat 37475 |
| [Baer] p. 44 | Part (1) | mapdpg 37514 |
| [Baer] p. 45 | Part (2) | hdmap1eq 37609 mapdheq 37536 mapdheq2 37537 mapdheq2biN 37538 |
| [Baer] p. 45 | Part (3) | baerlem3 37521 |
| [Baer] p. 46 | Part (4) | mapdheq4 37540 mapdheq4lem 37539 |
| [Baer] p. 46 | Part (5) | baerlem5a 37522 baerlem5abmN 37526 baerlem5amN 37524 baerlem5b 37523 baerlem5bmN 37525 |
| [Baer] p. 47 | Part (6) | hdmap1l6 37629 hdmap1l6a 37617 hdmap1l6e 37622 hdmap1l6f 37623 hdmap1l6g 37624 hdmap1l6lem1 37615 hdmap1l6lem2 37616 mapdh6N 37555 mapdh6aN 37543 mapdh6eN 37548 mapdh6fN 37549 mapdh6gN 37550 mapdh6lem1N 37541 mapdh6lem2N 37542 |
| [Baer] p. 48 | Part 9 | hdmapval 37636 |
| [Baer] p. 48 | Part 10 | hdmap10 37648 |
| [Baer] p. 48 | Part 11 | hdmapadd 37651 |
| [Baer] p. 48 | Part (6) | hdmap1l6h 37625 mapdh6hN 37551 |
| [Baer] p. 48 | Part (7) | mapdh75cN 37561 mapdh75d 37562 mapdh75e 37560 mapdh75fN 37563 mapdh7cN 37557 mapdh7dN 37558 mapdh7eN 37556 mapdh7fN 37559 |
| [Baer] p. 48 | Part (8) | mapdh8 37596 mapdh8a 37583 mapdh8aa 37584 mapdh8ab 37585 mapdh8ac 37586 mapdh8ad 37587 mapdh8b 37588 mapdh8c 37589 mapdh8d 37591 mapdh8d0N 37590 mapdh8e 37592 mapdh8g 37593 mapdh8i 37594 mapdh8j 37595 |
| [Baer] p. 48 | Part (9) | mapdh9a 37597 |
| [Baer] p. 48 | Equation 10 | mapdhvmap 37577 |
| [Baer] p. 49 | Part 12 | hdmap11 37656 hdmapeq0 37652 hdmapf1oN 37673 hdmapneg 37654 hdmaprnN 37672 hdmaprnlem1N 37657 hdmaprnlem3N 37658 hdmaprnlem3uN 37659 hdmaprnlem4N 37661 hdmaprnlem6N 37662 hdmaprnlem7N 37663 hdmaprnlem8N 37664 hdmaprnlem9N 37665 hdmapsub 37655 |
| [Baer] p. 49 | Part 14 | hdmap14lem1 37676 hdmap14lem10 37685 hdmap14lem1a 37674 hdmap14lem2N 37677 hdmap14lem2a 37675 hdmap14lem3 37678 hdmap14lem8 37683 hdmap14lem9 37684 |
| [Baer] p. 50 | Part 14 | hdmap14lem11 37686 hdmap14lem12 37687 hdmap14lem13 37688 hdmap14lem14 37689 hdmap14lem15 37690 hgmapval 37695 |
| [Baer] p. 50 | Part 15 | hgmapadd 37702 hgmapmul 37703 hgmaprnlem2N 37705 hgmapvs 37699 |
| [Baer] p. 50 | Part 16 | hgmaprnN 37709 |
| [Baer] p. 110 | Lemma 1 | hdmapip0com 37725 |
| [Baer] p. 110 | Line 27 | hdmapinvlem1 37726 |
| [Baer] p. 110 | Line 28 | hdmapinvlem2 37727 |
| [Baer] p. 110 | Line 30 | hdmapinvlem3 37728 |
| [Baer] p. 110 | Part 1.2 | hdmapglem5 37730 hgmapvv 37734 |
| [Baer] p. 110 | Proposition 1 | hdmapinvlem4 37729 |
| [Baer] p. 111 | Line 10 | hgmapvvlem1 37731 |
| [Baer] p. 111 | Line 15 | hdmapg 37738 hdmapglem7 37737 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 23 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2622 |
| [BellMachover] p. 460 | Notation | df-mo 2623 |
| [BellMachover] p. 460 | Definition | mo3 2656 |
| [BellMachover] p. 461 | Axiom Ext | ax-ext 2751 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2756 |
| [BellMachover] p. 463 | Axiom Rep | axrep5 4911 |
| [BellMachover] p. 463 | Scheme Sep | axsep 4915 |
| [BellMachover] p. 463 | Theorem 1.3(ii) | bj-bm1.3ii 33354 bm1.3ii 4919 |
| [BellMachover] p. 466 | Problem | axpow2 4977 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4978 |
| [BellMachover] p. 466 | Axiom Union | axun2 7102 |
| [BellMachover] p. 468 | Definition | df-ord 5868 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 5883 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 5890 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 5885 |
| [BellMachover] p. 471 | Definition of N | df-om 7217 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 7157 |
| [BellMachover] p. 471 | Definition of Lim | df-lim 5870 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 8707 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 7231 |
| [BellMachover] p. 477 | Equation 3.1 | df-r1 8795 |
| [BellMachover] p. 478 | Definition | rankval2 8849 |
| [BellMachover] p. 478 | Theorem 3.3(i) | r1ord3 8813 r1ord3g 8810 |
| [BellMachover] p. 480 | Axiom Reg | zfreg 8660 |
| [BellMachover] p. 488 | Axiom AC | ac5 9505 dfac4 9149 |
| [BellMachover] p. 490 | Definition of aleph | alephval3 9137 |
| [BeltramettiCassinelli] p. 98 | Remark | atlatmstc 35126 |
| [BeltramettiCassinelli] p. 107 | Remark 10.3.5 | atom1d 29552 |
| [BeltramettiCassinelli] p. 166 | Theorem 14.8.4 | chirred 29594 chirredi 29593 |
| [BeltramettiCassinelli1] p. 400 | Proposition P8(ii) | atoml2i 29582 |
| [Beran] p. 3 | Definition of join | sshjval3 28553 |
| [Beran] p. 39 | Theorem 2.3(i) | cmcm2 28815 cmcm2i 28792 cmcm2ii 28797 cmt2N 35057 |
| [Beran] p. 40 | Theorem 2.3(iii) | lecm 28816 lecmi 28801 lecmii 28802 |
| [Beran] p. 45 | Theorem 3.4 | cmcmlem 28790 |
| [Beran] p. 49 | Theorem 4.2 | cm2j 28819 cm2ji 28824 cm2mi 28825 |
| [Beran] p. 95 | Definition | df-sh 28404 issh2 28406 |
| [Beran] p. 95 | Lemma 3.1(S5) | his5 28283 |
| [Beran] p. 95 | Lemma 3.1(S6) | his6 28296 |
| [Beran] p. 95 | Lemma 3.1(S7) | his7 28287 |
| [Beran] p. 95 | Lemma 3.2(S8) | ho01i 29027 |
| [Beran] p. 95 | Lemma 3.2(S9) | hoeq1 29029 |
| [Beran] p. 95 | Lemma 3.2(S10) | ho02i 29028 |
| [Beran] p. 95 | Lemma 3.2(S11) | hoeq2 29030 |
| [Beran] p. 95 | Postulate (S1) | ax-his1 28279 his1i 28297 |
| [Beran] p. 95 | Postulate (S2) | ax-his2 28280 |
| [Beran] p. 95 | Postulate (S3) | ax-his3 28281 |
| [Beran] p. 95 | Postulate (S4) | ax-his4 28282 |
| [Beran] p. 96 | Definition of norm | df-hnorm 28165 dfhnorm2 28319 normval 28321 |
| [Beran] p. 96 | Definition for Cauchy sequence | hcau 28381 |
| [Beran] p. 96 | Definition of Cauchy sequence | df-hcau 28170 |
| [Beran] p. 96 | Definition of complete subspace | isch3 28438 |
| [Beran] p. 96 | Definition of converge | df-hlim 28169 hlimi 28385 |
| [Beran] p. 97 | Theorem 3.3(i) | norm-i-i 28330 norm-i 28326 |
| [Beran] p. 97 | Theorem 3.3(ii) | norm-ii-i 28334 norm-ii 28335 normlem0 28306 normlem1 28307 normlem2 28308 normlem3 28309 normlem4 28310 normlem5 28311 normlem6 28312 normlem7 28313 normlem7tALT 28316 |
| [Beran] p. 97 | Theorem 3.3(iii) | norm-iii-i 28336 norm-iii 28337 |
| [Beran] p. 98 | Remark 3.4 | bcs 28378 bcsiALT 28376 bcsiHIL 28377 |
| [Beran] p. 98 | Remark 3.4(B) | normlem9at 28318 normpar 28352 normpari 28351 |
| [Beran] p. 98 | Remark 3.4(C) | normpyc 28343 normpyth 28342 normpythi 28339 |
| [Beran] p. 99 | Remark | lnfn0 29246 lnfn0i 29241 lnop0 29165 lnop0i 29169 |
| [Beran] p. 99 | Theorem 3.5(i) | nmcexi 29225 nmcfnex 29252 nmcfnexi 29250 nmcopex 29228 nmcopexi 29226 |
| [Beran] p. 99 | Theorem 3.5(ii) | nmcfnlb 29253 nmcfnlbi 29251 nmcoplb 29229 nmcoplbi 29227 |
| [Beran] p. 99 | Theorem 3.5(iii) | lnfncon 29255 lnfnconi 29254 lnopcon 29234 lnopconi 29233 |
| [Beran] p. 100 | Lemma 3.6 | normpar2i 28353 |
| [Beran] p. 101 | Lemma 3.6 | norm3adifi 28350 norm3adifii 28345 norm3dif 28347 norm3difi 28344 |
| [Beran] p. 102 | Theorem 3.7(i) | chocunii 28500 pjhth 28592 pjhtheu 28593 pjpjhth 28624 pjpjhthi 28625 pjth 23429 |
| [Beran] p. 102 | Theorem 3.7(ii) | ococ 28605 ococi 28604 |
| [Beran] p. 103 | Remark 3.8 | nlelchi 29260 |
| [Beran] p. 104 | Theorem 3.9 | riesz3i 29261 riesz4 29263 riesz4i 29262 |
| [Beran] p. 104 | Theorem 3.10 | cnlnadj 29278 cnlnadjeu 29277 cnlnadjeui 29276 cnlnadji 29275 cnlnadjlem1 29266 nmopadjlei 29287 |
| [Beran] p. 106 | Theorem 3.11(i) | adjeq0 29290 |
| [Beran] p. 106 | Theorem 3.11(v) | nmopadji 29289 |
| [Beran] p. 106 | Theorem 3.11(ii) | adjmul 29291 |
| [Beran] p. 106 | Theorem 3.11(iv) | adjadj 29135 |
| [Beran] p. 106 | Theorem 3.11(vi) | nmopcoadj2i 29301 nmopcoadji 29300 |
| [Beran] p. 106 | Theorem 3.11(iii) | adjadd 29292 |
| [Beran] p. 106 | Theorem 3.11(vii) | nmopcoadj0i 29302 |
| [Beran] p. 106 | Theorem 3.11(viii) | adjcoi 29299 pjadj2coi 29403 pjadjcoi 29360 |
| [Beran] p. 107 | Definition | df-ch 28418 isch2 28420 |
| [Beran] p. 107 | Remark 3.12 | choccl 28505 isch3 28438 occl 28503 ocsh 28482 shoccl 28504 shocsh 28483 |
| [Beran] p. 107 | Remark 3.12(B) | ococin 28607 |
| [Beran] p. 108 | Theorem 3.13 | chintcl 28531 |
| [Beran] p. 109 | Property (i) | pjadj2 29386 pjadj3 29387 pjadji 28884 pjadjii 28873 |
| [Beran] p. 109 | Property (ii) | pjidmco 29380 pjidmcoi 29376 pjidmi 28872 |
| [Beran] p. 110 | Definition of projector ordering | pjordi 29372 |
| [Beran] p. 111 | Remark | ho0val 28949 pjch1 28869 |
| [Beran] p. 111 | Definition | df-hfmul 28933 df-hfsum 28932 df-hodif 28931 df-homul 28930 df-hosum 28929 |
| [Beran] p. 111 | Lemma 4.4(i) | pjo 28870 |
| [Beran] p. 111 | Lemma 4.4(ii) | pjch 28893 pjchi 28631 |
| [Beran] p. 111 | Lemma 4.4(iii) | pjoc2 28638 pjoc2i 28637 |
| [Beran] p. 112 | Theorem 4.5(i)->(ii) | pjss2i 28879 |
| [Beran] p. 112 | Theorem 4.5(i)->(iv) | pjssmi 29364 pjssmii 28880 |
| [Beran] p. 112 | Theorem 4.5(i)<->(ii) | pjss2coi 29363 |
| [Beran] p. 112 | Theorem 4.5(i)<->(iii) | pjss1coi 29362 |
| [Beran] p. 112 | Theorem 4.5(i)<->(vi) | pjnormssi 29367 |
| [Beran] p. 112 | Theorem 4.5(iv)->(v) | pjssge0i 29365 pjssge0ii 28881 |
| [Beran] p. 112 | Theorem 4.5(v)<->(vi) | pjdifnormi 29366 pjdifnormii 28882 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1849 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1847 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1850 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1845 |
| [Bogachev] p. 16 | Definition 1.5 | df-oms 30694 |
| [Bogachev] p. 17 | Lemma 1.5.4 | omssubadd 30702 |
| [Bogachev] p. 17 | Example 1.5.2 | omsmon 30700 |
| [Bogachev] p. 41 | Definition 1.11.2 | df-carsg 30704 |
| [Bogachev] p. 42 | Theorem 1.11.4 | carsgsiga 30724 |
| [Bogachev] p. 116 | Definition 2.3.1 | df-itgm 30755 df-sitm 30733 |
| [Bogachev] p. 118 | Chapter 2.4.4 | df-itgm 30755 |
| [Bogachev] p. 118 | Definition 2.4.1 | df-sitg 30732 |
| [Bollobas] p. 1 | Section I.1 | df-edg 26161 isuhgrop 26186 isusgrop 26279 isuspgrop 26278 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 26383 uhgrspan1 26418 uhgrspansubgr 26406 |
| [Bollobas] p. 3 | Section I.1 | cusgrsize 26585 df-cusgr 26542 df-nbgr 26448 fusgrmaxsize 26595 |
| [Bollobas] p. 4 | Definition | df-upwlks 42238 df-wlks 26730 |
| [Bollobas] p. 4 | Section I.1 | finsumvtxdg2size 26681 finsumvtxdgeven 26683 fusgr1th 26682 fusgrvtxdgonume 26685 vtxdgoddnumeven 26684 |
| [Bollobas] p. 5 | Notation | df-pths 26847 |
| [Bollobas] p. 5 | Definition | df-crcts 26917 df-cycls 26918 df-trls 26824 df-wlkson 26731 |
| [Bollobas] p. 7 | Section I.1 | df-ushgr 26175 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-clintop 42359 df-cllaw 42345 df-mgm 17450 df-mgm2 42378 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-assintop 42360 df-asslaw 42347 df-sgrp 17492 df-sgrp2 42380 |
| [BourbakiAlg1] p. 7 | Definition 8 | df-cmgm2 42379 df-comlaw 42346 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 17503 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 18757 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng0 42398 |
| [BourbakiEns] p. | Proposition 8 | fcof1 6688 fcofo 6689 |
| [BourbakiTop1] p. | Remark | xnegmnf 12246 xnegpnf 12245 |
| [BourbakiTop1] p. | Remark | rexneg 12247 |
| [BourbakiTop1] p. | Remark 3 | ust0 22243 ustfilxp 22236 |
| [BourbakiTop1] p. | Axiom GT' | tgpsubcn 22114 |
| [BourbakiTop1] p. | Example 1 | cstucnd 22308 iducn 22307 snfil 21888 |
| [BourbakiTop1] p. | Example 2 | neifil 21904 |
| [BourbakiTop1] p. | Theorem 1 | cnextcn 22091 |
| [BourbakiTop1] p. | Theorem 2 | ucnextcn 22328 |
| [BourbakiTop1] p. | Theorem 3 | df-hcmp 30343 |
| [BourbakiTop1] p. | Paragraph 3 | infil 21887 |
| [BourbakiTop1] p. | Proposition | ishmeo 21783 |
| [BourbakiTop1] p. | Definition 1 | df-ucn 22300 df-ust 22224 filintn0 21885 filn0 21886 istgp 22101 ucnprima 22306 |
| [BourbakiTop1] p. | Definition 2 | df-cfilu 22311 |
| [BourbakiTop1] p. | Definition 3 | df-cusp 22322 df-usp 22281 df-utop 22255 trust 22253 |
| [BourbakiTop1] p. | Definition 6 | df-pcmp 30263 |
| [BourbakiTop1] p. | Property V_i | ssnei2 21141 |
| [BourbakiTop1] p. | Theorem 1(d) | iscncl 21294 |
| [BourbakiTop1] p. | Condition F_I | ustssel 22229 |
| [BourbakiTop1] p. | Condition U_I | ustdiag 22232 |
| [BourbakiTop1] p. | Property V_ii | innei 21150 |
| [BourbakiTop1] p. | Property V_iv | neiptopreu 21158 neissex 21152 |
| [BourbakiTop1] p. | Proposition 1 | neips 21138 neiss 21134 ucncn 22309 ustund 22245 ustuqtop 22270 |
| [BourbakiTop1] p. | Proposition 2 | cnpco 21292 neiptopreu 21158 utop2nei 22274 utop3cls 22275 |
| [BourbakiTop1] p. | Proposition 3 | fmucnd 22316 uspreg 22298 utopreg 22276 |
| [BourbakiTop1] p. | Proposition 4 | imasncld 21715 imasncls 21716 imasnopn 21714 |
| [BourbakiTop1] p. | Proposition 9 | cnpflf2 22024 |
| [BourbakiTop1] p. | Condition F_II | ustincl 22231 |
| [BourbakiTop1] p. | Condition U_II | ustinvel 22233 |
| [BourbakiTop1] p. | Property V_iii | elnei 21136 |
| [BourbakiTop1] p. | Proposition 11 | cnextucn 22327 |
| [BourbakiTop1] p. | Condition F_IIb | ustbasel 22230 |
| [BourbakiTop1] p. | Condition U_III | ustexhalf 22234 |
| [BourbakiTop1] p. | Definition C''' | df-cmp 21411 |
| [BourbakiTop1] p. | Axioms FI, FIIa, FIIb, FIII) | df-fil 21870 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 20919 |
| [BourbakiTop2] p. 195 | Definition 1 | df-ldlf 30260 |
| [BrosowskiDeutsh] p. 89 | Proof follows | stoweidlem62 40791 |
| [BrosowskiDeutsh] p. 89 | Lemmas are written following | stowei 40793 stoweid 40792 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem1 40730 stoweidlem10 40739 stoweidlem14 40743 stoweidlem15 40744 stoweidlem35 40764 stoweidlem36 40765 stoweidlem37 40766 stoweidlem38 40767 stoweidlem40 40769 stoweidlem41 40770 stoweidlem43 40772 stoweidlem44 40773 stoweidlem46 40775 stoweidlem5 40734 stoweidlem50 40779 stoweidlem52 40781 stoweidlem53 40782 stoweidlem55 40784 stoweidlem56 40785 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem23 40752 stoweidlem24 40753 stoweidlem27 40756 stoweidlem28 40757 stoweidlem30 40759 |
| [BrosowskiDeutsh] p. 91 | Proof | stoweidlem34 40763 stoweidlem59 40788 stoweidlem60 40789 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem45 40774 stoweidlem49 40778 stoweidlem7 40736 |
| [BrosowskiDeutsh] p. 91 | Lemma 2 | stoweidlem31 40760 stoweidlem39 40768 stoweidlem42 40771 stoweidlem48 40777 stoweidlem51 40780 stoweidlem54 40783 stoweidlem57 40786 stoweidlem58 40787 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem25 40754 |
| [BrosowskiDeutsh] p. 91 | Lemma proves that the function ` ` (as defined | stoweidlem17 40746 |
| [BrosowskiDeutsh] p. 92 | Proof | stoweidlem11 40740 stoweidlem13 40742 stoweidlem26 40755 stoweidlem61 40790 |
| [BrosowskiDeutsh] p. 92 | Lemma 2 | stoweidlem18 40747 |
| [Bruck] p. 1 | Section I.1 | df-clintop 42359 df-mgm 17450 df-mgm2 42378 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 17492 df-sgrp2 42380 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3 17722 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4865 |
| [Church] p. 129 | Section II.24 | df-ifp 1050 dfifp2 1051 |
| [Clemente] p. 10 | Definition IT | natded 27602 |
| [Clemente] p. 10 | Definition I` `m,n | natded 27602 |
| [Clemente] p. 11 | Definition E=>m,n | natded 27602 |
| [Clemente] p. 11 | Definition I=>m,n | natded 27602 |
| [Clemente] p. 11 | Definition E` `(1) | natded 27602 |
| [Clemente] p. 11 | Definition E` `(2) | natded 27602 |
| [Clemente] p. 12 | Definition E` `m,n,p | natded 27602 |
| [Clemente] p. 12 | Definition I` `n(1) | natded 27602 |
| [Clemente] p. 12 | Definition I` `n(2) | natded 27602 |
| [Clemente] p. 13 | Definition I` `m,n,p | natded 27602 |
| [Clemente] p. 14 | Proof 5.11 | natded 27602 |
| [Clemente] p. 14 | Definition E` `n | natded 27602 |
| [Clemente] p. 15 | Theorem 5.2 | ex-natded5.2-2 27604 ex-natded5.2 27603 |
| [Clemente] p. 16 | Theorem 5.3 | ex-natded5.3-2 27607 ex-natded5.3 27606 |
| [Clemente] p. 18 | Theorem 5.5 | ex-natded5.5 27609 |
| [Clemente] p. 19 | Theorem 5.7 | ex-natded5.7-2 27611 ex-natded5.7 27610 |
| [Clemente] p. 20 | Theorem 5.8 | ex-natded5.8-2 27613 ex-natded5.8 27612 |
| [Clemente] p. 20 | Theorem 5.13 | ex-natded5.13-2 27615 ex-natded5.13 27614 |
| [Clemente] p. 32 | Definition I` `n | natded 27602 |
| [Clemente] p. 32 | Definition E` `m,n,p,a | natded 27602 |
| [Clemente] p. 32 | Definition E` `n,t | natded 27602 |
| [Clemente] p. 32 | Definition I` `n,t | natded 27602 |
| [Clemente] p. 43 | Theorem 9.20 | ex-natded9.20 27616 |
| [Clemente] p. 45 | Theorem 9.20 | ex-natded9.20-2 27617 |
| [Clemente] p. 45 | Theorem 9.26 | ex-natded9.26-2 27619 ex-natded9.26 27618 |
| [Cohen] p. 301 | Remark | relogoprlem 24558 |
| [Cohen] p. 301 | Property 2 | relogmul 24559 relogmuld 24592 |
| [Cohen] p. 301 | Property 3 | relogdiv 24560 relogdivd 24593 |
| [Cohen] p. 301 | Property 4 | relogexp 24563 |
| [Cohen] p. 301 | Property 1a | log1 24553 |
| [Cohen] p. 301 | Property 1b | loge 24554 |
| [Cohen4] p. 348 | Observation | relogbcxpb 24746 |
| [Cohen4] p. 349 | Property | relogbf 24750 |
| [Cohen4] p. 352 | Definition | elogb 24729 |
| [Cohen4] p. 361 | Property 2 | relogbmul 24736 |
| [Cohen4] p. 361 | Property 3 | logbrec 24741 relogbdiv 24738 |
| [Cohen4] p. 361 | Property 4 | relogbreexp 24734 |
| [Cohen4] p. 361 | Property 6 | relogbexp 24739 |
| [Cohen4] p. 361 | Property 1(a) | logbid1 24727 |
| [Cohen4] p. 361 | Property 1(b) | logb1 24728 |
| [Cohen4] p. 367 | Property | logbchbase 24730 |
| [Cohen4] p. 377 | Property 2 | logblt 24743 |
| [Cohn] p. 4 | Proposition 1.1.5 | sxbrsigalem1 30687 sxbrsigalem4 30689 |
| [Cohn] p. 81 | Section II.5 | acsdomd 17389 acsinfd 17388 acsinfdimd 17390 acsmap2d 17387 acsmapd 17386 |
| [Cohn] p. 143 | Example 5.1.1 | sxbrsiga 30692 |
| [Connell] p. 57 | Definition | df-scmat 20515 df-scmatalt 42711 |
| [CormenLeisersonRivest] p. 33 | Equation 2.4 | fldiv2 12868 |
| [Crawley] p. 1 | Definition of poset | df-poset 17154 |
| [Crawley] p. 107 | Theorem 13.2 | hlsupr 35193 |
| [Crawley] p. 110 | Theorem 13.3 | arglem1N 35998 dalaw 35693 |
| [Crawley] p. 111 | Theorem 13.4 | hlathil 37769 |
| [Crawley] p. 111 | Definition of set W | df-watsN 35797 |
| [Crawley] p. 111 | Definition of dilation | df-dilN 35913 df-ldil 35911 isldil 35917 |
| [Crawley] p. 111 | Definition of translation | df-ltrn 35912 df-trnN 35914 isltrn 35926 ltrnu 35928 |
| [Crawley] p. 112 | Lemma A | cdlema1N 35598 cdlema2N 35599 exatleN 35211 |
| [Crawley] p. 112 | Lemma B | 1cvrat 35283 cdlemb 35601 cdlemb2 35848 cdlemb3 36414 idltrn 35957 l1cvat 34862 lhpat 35850 lhpat2 35852 lshpat 34863 ltrnel 35946 ltrnmw 35958 |
| [Crawley] p. 112 | Lemma C | cdlemc1 35999 cdlemc2 36000 ltrnnidn 35982 trlat 35977 trljat1 35974 trljat2 35975 trljat3 35976 trlne 35993 trlnidat 35981 trlnle 35994 |
| [Crawley] p. 112 | Definition of automorphism | df-pautN 35798 |
| [Crawley] p. 113 | Lemma C | cdlemc 36005 cdlemc3 36001 cdlemc4 36002 |
| [Crawley] p. 113 | Lemma D | cdlemd 36015 cdlemd1 36006 cdlemd2 36007 cdlemd3 36008 cdlemd4 36009 cdlemd5 36010 cdlemd6 36011 cdlemd7 36012 cdlemd8 36013 cdlemd9 36014 cdleme31sde 36193 cdleme31se 36190 cdleme31se2 36191 cdleme31snd 36194 cdleme32a 36249 cdleme32b 36250 cdleme32c 36251 cdleme32d 36252 cdleme32e 36253 cdleme32f 36254 cdleme32fva 36245 cdleme32fva1 36246 cdleme32fvcl 36248 cdleme32le 36255 cdleme48fv 36307 cdleme4gfv 36315 cdleme50eq 36349 cdleme50f 36350 cdleme50f1 36351 cdleme50f1o 36354 cdleme50laut 36355 cdleme50ldil 36356 cdleme50lebi 36348 cdleme50rn 36353 cdleme50rnlem 36352 cdlemeg49le 36319 cdlemeg49lebilem 36347 |
| [Crawley] p. 113 | Lemma E | cdleme 36368 cdleme00a 36017 cdleme01N 36029 cdleme02N 36030 cdleme0a 36019 cdleme0aa 36018 cdleme0b 36020 cdleme0c 36021 cdleme0cp 36022 cdleme0cq 36023 cdleme0dN 36024 cdleme0e 36025 cdleme0ex1N 36031 cdleme0ex2N 36032 cdleme0fN 36026 cdleme0gN 36027 cdleme0moN 36033 cdleme1 36035 cdleme10 36062 cdleme10tN 36066 cdleme11 36078 cdleme11a 36068 cdleme11c 36069 cdleme11dN 36070 cdleme11e 36071 cdleme11fN 36072 cdleme11g 36073 cdleme11h 36074 cdleme11j 36075 cdleme11k 36076 cdleme11l 36077 cdleme12 36079 cdleme13 36080 cdleme14 36081 cdleme15 36086 cdleme15a 36082 cdleme15b 36083 cdleme15c 36084 cdleme15d 36085 cdleme16 36093 cdleme16aN 36067 cdleme16b 36087 cdleme16c 36088 cdleme16d 36089 cdleme16e 36090 cdleme16f 36091 cdleme16g 36092 cdleme19a 36111 cdleme19b 36112 cdleme19c 36113 cdleme19d 36114 cdleme19e 36115 cdleme19f 36116 cdleme1b 36034 cdleme2 36036 cdleme20aN 36117 cdleme20bN 36118 cdleme20c 36119 cdleme20d 36120 cdleme20e 36121 cdleme20f 36122 cdleme20g 36123 cdleme20h 36124 cdleme20i 36125 cdleme20j 36126 cdleme20k 36127 cdleme20l 36130 cdleme20l1 36128 cdleme20l2 36129 cdleme20m 36131 cdleme20y 36110 cdleme20zN 36109 cdleme21 36145 cdleme21d 36138 cdleme21e 36139 cdleme22a 36148 cdleme22aa 36147 cdleme22b 36149 cdleme22cN 36150 cdleme22d 36151 cdleme22e 36152 cdleme22eALTN 36153 cdleme22f 36154 cdleme22f2 36155 cdleme22g 36156 cdleme23a 36157 cdleme23b 36158 cdleme23c 36159 cdleme26e 36167 cdleme26eALTN 36169 cdleme26ee 36168 cdleme26f 36171 cdleme26f2 36173 cdleme26f2ALTN 36172 cdleme26fALTN 36170 cdleme27N 36177 cdleme27a 36175 cdleme27cl 36174 cdleme28c 36180 cdleme3 36045 cdleme30a 36186 cdleme31fv 36198 cdleme31fv1 36199 cdleme31fv1s 36200 cdleme31fv2 36201 cdleme31id 36202 cdleme31sc 36192 cdleme31sdnN 36195 cdleme31sn 36188 cdleme31sn1 36189 cdleme31sn1c 36196 cdleme31sn2 36197 cdleme31so 36187 cdleme35a 36256 cdleme35b 36258 cdleme35c 36259 cdleme35d 36260 cdleme35e 36261 cdleme35f 36262 cdleme35fnpq 36257 cdleme35g 36263 cdleme35h 36264 cdleme35h2 36265 cdleme35sn2aw 36266 cdleme35sn3a 36267 cdleme36a 36268 cdleme36m 36269 cdleme37m 36270 cdleme38m 36271 cdleme38n 36272 cdleme39a 36273 cdleme39n 36274 cdleme3b 36037 cdleme3c 36038 cdleme3d 36039 cdleme3e 36040 cdleme3fN 36041 cdleme3fa 36044 cdleme3g 36042 cdleme3h 36043 cdleme4 36046 cdleme40m 36275 cdleme40n 36276 cdleme40v 36277 cdleme40w 36278 cdleme41fva11 36285 cdleme41sn3aw 36282 cdleme41sn4aw 36283 cdleme41snaw 36284 cdleme42a 36279 cdleme42b 36286 cdleme42c 36280 cdleme42d 36281 cdleme42e 36287 cdleme42f 36288 cdleme42g 36289 cdleme42h 36290 cdleme42i 36291 cdleme42k 36292 cdleme42ke 36293 cdleme42keg 36294 cdleme42mN 36295 cdleme42mgN 36296 cdleme43aN 36297 cdleme43bN 36298 cdleme43cN 36299 cdleme43dN 36300 cdleme5 36048 cdleme50ex 36367 cdleme50ltrn 36365 cdleme51finvN 36364 cdleme51finvfvN 36363 cdleme51finvtrN 36366 cdleme6 36049 cdleme7 36057 cdleme7a 36051 cdleme7aa 36050 cdleme7b 36052 cdleme7c 36053 cdleme7d 36054 cdleme7e 36055 cdleme7ga 36056 cdleme8 36058 cdleme8tN 36063 cdleme9 36061 cdleme9a 36059 cdleme9b 36060 cdleme9tN 36065 cdleme9taN 36064 cdlemeda 36106 cdlemedb 36105 cdlemednpq 36107 cdlemednuN 36108 cdlemefr27cl 36211 cdlemefr32fva1 36218 cdlemefr32fvaN 36217 cdlemefrs32fva 36208 cdlemefrs32fva1 36209 cdlemefs27cl 36221 cdlemefs32fva1 36231 cdlemefs32fvaN 36230 cdlemesner 36104 cdlemeulpq 36028 |
| [Crawley] p. 114 | Lemma E | 4atex 35883 4atexlem7 35882 cdleme0nex 36098 cdleme17a 36094 cdleme17c 36096 cdleme17d 36306 cdleme17d1 36097 cdleme17d2 36303 cdleme18a 36099 cdleme18b 36100 cdleme18c 36101 cdleme18d 36103 cdleme4a 36047 |
| [Crawley] p. 115 | Lemma E | cdleme21a 36133 cdleme21at 36136 cdleme21b 36134 cdleme21c 36135 cdleme21ct 36137 cdleme21f 36140 cdleme21g 36141 cdleme21h 36142 cdleme21i 36143 cdleme22gb 36102 |
| [Crawley] p. 116 | Lemma F | cdlemf 36371 cdlemf1 36369 cdlemf2 36370 |
| [Crawley] p. 116 | Lemma G | cdlemftr1 36375 cdlemg16 36465 cdlemg28 36512 cdlemg28a 36501 cdlemg28b 36511 cdlemg3a 36405 cdlemg42 36537 cdlemg43 36538 cdlemg44 36541 cdlemg44a 36539 cdlemg46 36543 cdlemg47 36544 cdlemg9 36442 ltrnco 36527 ltrncom 36546 tgrpabl 36559 trlco 36535 |
| [Crawley] p. 116 | Definition of G | df-tgrp 36551 |
| [Crawley] p. 117 | Lemma G | cdlemg17 36485 cdlemg17b 36470 |
| [Crawley] p. 117 | Definition of E | df-edring-rN 36564 df-edring 36565 |
| [Crawley] p. 117 | Definition of trace-preserving endomorphism | istendo 36568 |
| [Crawley] p. 118 | Remark | tendopltp 36588 |
| [Crawley] p. 118 | Lemma H | cdlemh 36625 cdlemh1 36623 cdlemh2 36624 |
| [Crawley] p. 118 | Lemma I | cdlemi 36628 cdlemi1 36626 cdlemi2 36627 |
| [Crawley] p. 118 | Lemma J | cdlemj1 36629 cdlemj2 36630 cdlemj3 36631 tendocan 36632 |
| [Crawley] p. 118 | Lemma K | cdlemk 36782 cdlemk1 36639 cdlemk10 36651 cdlemk11 36657 cdlemk11t 36754 cdlemk11ta 36737 cdlemk11tb 36739 cdlemk11tc 36753 cdlemk11u-2N 36697 cdlemk11u 36679 cdlemk12 36658 cdlemk12u-2N 36698 cdlemk12u 36680 cdlemk13-2N 36684 cdlemk13 36660 cdlemk14-2N 36686 cdlemk14 36662 cdlemk15-2N 36687 cdlemk15 36663 cdlemk16-2N 36688 cdlemk16 36665 cdlemk16a 36664 cdlemk17-2N 36689 cdlemk17 36666 cdlemk18-2N 36694 cdlemk18-3N 36708 cdlemk18 36676 cdlemk19-2N 36695 cdlemk19 36677 cdlemk19u 36778 cdlemk1u 36667 cdlemk2 36640 cdlemk20-2N 36700 cdlemk20 36682 cdlemk21-2N 36699 cdlemk21N 36681 cdlemk22-3 36709 cdlemk22 36701 cdlemk23-3 36710 cdlemk24-3 36711 cdlemk25-3 36712 cdlemk26-3 36714 cdlemk26b-3 36713 cdlemk27-3 36715 cdlemk28-3 36716 cdlemk29-3 36719 cdlemk3 36641 cdlemk30 36702 cdlemk31 36704 cdlemk32 36705 cdlemk33N 36717 cdlemk34 36718 cdlemk35 36720 cdlemk36 36721 cdlemk37 36722 cdlemk38 36723 cdlemk39 36724 cdlemk39u 36776 cdlemk4 36642 cdlemk41 36728 cdlemk42 36749 cdlemk42yN 36752 cdlemk43N 36771 cdlemk45 36755 cdlemk46 36756 cdlemk47 36757 cdlemk48 36758 cdlemk49 36759 cdlemk5 36644 cdlemk50 36760 cdlemk51 36761 cdlemk52 36762 cdlemk53 36765 cdlemk54 36766 cdlemk55 36769 cdlemk55u 36774 cdlemk56 36779 cdlemk5a 36643 cdlemk5auN 36668 cdlemk5u 36669 cdlemk6 36645 cdlemk6u 36670 cdlemk7 36656 cdlemk7u-2N 36696 cdlemk7u 36678 cdlemk8 36646 cdlemk9 36647 cdlemk9bN 36648 cdlemki 36649 cdlemkid 36744 cdlemkj-2N 36690 cdlemkj 36671 cdlemksat 36654 cdlemksel 36653 cdlemksv 36652 cdlemksv2 36655 cdlemkuat 36674 cdlemkuel-2N 36692 cdlemkuel-3 36706 cdlemkuel 36673 cdlemkuv-2N 36691 cdlemkuv2-2 36693 cdlemkuv2-3N 36707 cdlemkuv2 36675 cdlemkuvN 36672 cdlemkvcl 36650 cdlemky 36734 cdlemkyyN 36770 tendoex 36783 |
| [Crawley] p. 120 | Remark | dva1dim 36793 |
| [Crawley] p. 120 | Lemma L | cdleml1N 36784 cdleml2N 36785 cdleml3N 36786 cdleml4N 36787 cdleml5N 36788 cdleml6 36789 cdleml7 36790 cdleml8 36791 cdleml9 36792 dia1dim 36869 |
| [Crawley] p. 120 | Lemma M | dia11N 36856 diaf11N 36857 dialss 36854 diaord 36855 dibf11N 36969 djajN 36945 |
| [Crawley] p. 120 | Definition of isomorphism map | diaval 36840 |
| [Crawley] p. 121 | Lemma M | cdlemm10N 36926 dia2dimlem1 36872 dia2dimlem2 36873 dia2dimlem3 36874 dia2dimlem4 36875 dia2dimlem5 36876 diaf1oN 36938 diarnN 36937 dvheveccl 36920 dvhopN 36924 |
| [Crawley] p. 121 | Lemma N | cdlemn 37020 cdlemn10 37014 cdlemn11 37019 cdlemn11a 37015 cdlemn11b 37016 cdlemn11c 37017 cdlemn11pre 37018 cdlemn2 37003 cdlemn2a 37004 cdlemn3 37005 cdlemn4 37006 cdlemn4a 37007 cdlemn5 37009 cdlemn5pre 37008 cdlemn6 37010 cdlemn7 37011 cdlemn8 37012 cdlemn9 37013 diclspsn 37002 |
| [Crawley] p. 121 | Definition of phi(q) | df-dic 36981 |
| [Crawley] p. 122 | Lemma N | dih11 37073 dihf11 37075 dihjust 37025 dihjustlem 37024 dihord 37072 dihord1 37026 dihord10 37031 dihord11b 37030 dihord11c 37032 dihord2 37035 dihord2a 37027 dihord2b 37028 dihord2cN 37029 dihord2pre 37033 dihord2pre2 37034 dihordlem6 37021 dihordlem7 37022 dihordlem7b 37023 |
| [Crawley] p. 122 | Definition of isomorphism map | dihffval 37038 dihfval 37039 dihval 37040 |
| [Diestel] p. 3 | Section 1.1 | df-cusgr 26542 df-nbgr 26448 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 26383 uhgrspan1 26418 uhgrspansubgr 26406 |
| [Diestel] p. 5 | Proposition 1.2.1 | fusgrvtxdgonume 26685 vtxdgoddnumeven 26684 |
| [Diestel] p. 27 | Section 1.10 | df-ushgr 26175 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3726 |
| [Eisenberg] p. 82 | Definition 6.3 | dfom3 8712 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 8015 |
| [Eisenberg] p. 216 | Example 13.2(4) | omenps 8720 |
| [Eisenberg] p. 310 | Theorem 19.8 | cardprc 9010 |
| [Eisenberg] p. 310 | Corollary 19.7(2) | cardsdom 9583 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4923 |
| [Enderton] p. 19 | Definition | df-tp 4322 |
| [Enderton] p. 26 | Exercise 5 | unissb 4606 |
| [Enderton] p. 26 | Exercise 10 | pwel 5049 |
| [Enderton] p. 28 | Exercise 7(b) | pwun 5156 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1 4726 iinin2 4725 iinun2 4721 iunin1 4720 iunin1f 29712 iunin2 4719 uniin1 29705 uniin2 29706 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2 4724 iundif2 4722 |
| [Enderton] p. 32 | Exercise 20 | unineq 4026 |
| [Enderton] p. 33 | Exercise 23 | iinuni 4744 |
| [Enderton] p. 33 | Exercise 25 | iununi 4745 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4752 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 7129 iunpwss 4753 |
| [Enderton] p. 36 | Definition | opthwiener 5108 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 5047 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4611 |
| [Enderton] p. 41 | Lemma 3D | opeluu 5067 rnex 7251 rnexg 7249 |
| [Enderton] p. 41 | Exercise 8 | dmuni 5471 rnuni 5684 |
| [Enderton] p. 42 | Definition of a function | dffun7 6057 dffun8 6058 |
| [Enderton] p. 43 | Definition of function value | funfv2 6410 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 6097 |
| [Enderton] p. 44 | Definition (d) | dfima2 5608 dfima3 5609 |
| [Enderton] p. 47 | Theorem 3H | fvco2 6417 |
| [Enderton] p. 49 | Axiom of Choice (first form) | ac7 9501 ac7g 9502 df-ac 9143 dfac2 9158 dfac2a 9156 dfac2b 9157 dfac3 9148 dfac7 9160 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 6650 |
| [Enderton] p. 52 | Definition | df-map 8015 |
| [Enderton] p. 53 | Exercise 21 | coass 5797 |
| [Enderton] p. 53 | Exercise 27 | dmco 5786 |
| [Enderton] p. 53 | Exercise 14(a) | funin 6104 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5641 |
| [Enderton] p. 54 | Remark | ixpf 8088 ixpssmap 8100 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 8067 |
| [Enderton] p. 55 | Axiom of Choice (second form) | ac9 9511 ac9s 9521 |
| [Enderton] p. 56 | Theorem 3M | erref 7920 |
| [Enderton] p. 57 | Lemma 3N | erthi 7949 |
| [Enderton] p. 57 | Definition | df-ec 7902 |
| [Enderton] p. 58 | Definition | df-qs 7906 |
| [Enderton] p. 61 | Exercise 35 | df-ec 7902 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 5468 |
| [Enderton] p. 68 | Definition of successor | df-suc 5871 |
| [Enderton] p. 71 | Definition | df-tr 4888 dftr4 4892 |
| [Enderton] p. 72 | Theorem 4E | unisuc 5943 |
| [Enderton] p. 73 | Exercise 6 | unisuc 5943 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4901 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4902 trintALT 39637 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 7842 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 7844 onasuc 7766 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6799 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 7843 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 7845 onmsuc 7767 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 7860 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 7847 nnacom 7855 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 7861 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 7862 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 7864 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 7848 nnmsucr 7863 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 7876 |
| [Enderton] p. 129 | Definition | df-en 8114 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 6754 |
| [Enderton] p. 133 | Exercise 1 | xpomen 9042 |
| [Enderton] p. 133 | Exercise 2 | qnnen 15148 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | php 8304 |
| [Enderton] p. 135 | Corollary 6C | php3 8306 |
| [Enderton] p. 136 | Corollary 6E | nneneq 8303 |
| [Enderton] p. 136 | Corollary 6D(a) | pssinf 8330 |
| [Enderton] p. 136 | Corollary 6D(b) | ominf 8332 |
| [Enderton] p. 137 | Lemma 6F | pssnn 8338 |
| [Enderton] p. 138 | Corollary 6G | ssfi 8340 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 8284 |
| [Enderton] p. 142 | Theorem 6I(3) | xpcdaen 9211 |
| [Enderton] p. 142 | Theorem 6I(4) | mapcdaen 9212 |
| [Enderton] p. 143 | Theorem 6J | cda0en 9207 cda1en 9203 |
| [Enderton] p. 144 | Exercise 13 | iunfi 8414 unifi 8415 unifi2 8416 |
| [Enderton] p. 144 | Corollary 6K | undif2 4187 unfi 8387 unfi2 8389 |
| [Enderton] p. 145 | Figure 38 | ffoss 7278 |
| [Enderton] p. 145 | Definition | df-dom 8115 |
| [Enderton] p. 146 | Example 1 | domen 8126 domeng 8127 |
| [Enderton] p. 146 | Example 3 | nndomo 8314 nnsdom 8719 nnsdomg 8379 |
| [Enderton] p. 149 | Theorem 6L(a) | cdadom2 9215 |
| [Enderton] p. 149 | Theorem 6L(c) | mapdom1 8285 xpdom1 8219 xpdom1g 8217 xpdom2g 8216 |
| [Enderton] p. 149 | Theorem 6L(d) | mapdom2 8291 |
| [Enderton] p. 151 | Theorem 6M | zorn 9535 zorng 9532 |
| [Enderton] p. 151 | Theorem 6M(4) | ac8 9520 dfac5 9155 |
| [Enderton] p. 159 | Theorem 6Q | unictb 9603 |
| [Enderton] p. 164 | Example | infdif 9237 |
| [Enderton] p. 168 | Definition | df-po 5171 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 5977 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 5913 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 5976 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 5920 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 7189 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 7138 |
| [Enderton] p. 194 | Remark | onprc 7135 |
| [Enderton] p. 194 | Exercise 16 | suc11 5973 |
| [Enderton] p. 197 | Definition | df-card 8969 |
| [Enderton] p. 197 | Theorem 7P | carden 9579 |
| [Enderton] p. 200 | Exercise 25 | tfis 7205 |
| [Enderton] p. 202 | Lemma 7T | r1tr 8807 |
| [Enderton] p. 202 | Definition | df-r1 8795 |
| [Enderton] p. 202 | Theorem 7Q | r1val1 8817 |
| [Enderton] p. 204 | Theorem 7V(b) | rankval4 8898 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 8670 |
| [Enderton] p. 207 | Exercise 30 | rankpr 8888 rankprb 8882 rankpw 8874 rankpwi 8854 rankuniss 8897 |
| [Enderton] p. 207 | Exercise 34 | opthreg 8681 |
| [Enderton] p. 208 | Exercise 35 | suc11reg 8684 |
| [Enderton] p. 212 | Definition of aleph | alephval3 9137 |
| [Enderton] p. 213 | Theorem 8A(a) | alephord2 9103 |
| [Enderton] p. 213 | Theorem 8A(b) | cardalephex 9117 |
| [Enderton] p. 218 | Theorem Schema 8E | onfununi 7595 |
| [Enderton] p. 222 | Definition of kard | karden 8926 kardex 8925 |
| [Enderton] p. 238 | Theorem 8R | oeoa 7835 |
| [Enderton] p. 238 | Theorem 8S | oeoe 7837 |
| [Enderton] p. 240 | Exercise 25 | oarec 7800 |
| [Enderton] p. 257 | Definition of cofinality | cflm 9278 |
| [FaureFrolicher] p. 57 | Definition 3.1.9 | mreexd 16510 |
| [FaureFrolicher] p. 83 | Definition 4.1.1 | df-mri 16456 |
| [FaureFrolicher] p. 83 | Proposition 4.1.3 | acsfiindd 17385 mrieqv2d 16507 mrieqvd 16506 |
| [FaureFrolicher] p. 84 | Lemma 4.1.5 | mreexmrid 16511 |
| [FaureFrolicher] p. 86 | Proposition 4.2.1 | mreexexd 16516 mreexexlem2d 16513 |
| [FaureFrolicher] p. 87 | Theorem 4.2.2 | acsexdimd 17391 mreexfidimd 16518 |
| [Frege1879] p. 11 | Statement | df3or2 38584 |
| [Frege1879] p. 12 | Statement | df3an2 38585 dfxor4 38582 dfxor5 38583 |
| [Frege1879] p. 26 | Axiom 1 | ax-frege1 38608 |
| [Frege1879] p. 26 | Axiom 2 | ax-frege2 38609 |
| [Frege1879] p. 26 | Proposition 1 | ax-1 6 |
| [Frege1879] p. 26 | Proposition 2 | ax-2 7 |
| [Frege1879] p. 29 | Proposition 3 | frege3 38613 |
| [Frege1879] p. 31 | Proposition 4 | frege4 38617 |
| [Frege1879] p. 32 | Proposition 5 | frege5 38618 |
| [Frege1879] p. 33 | Proposition 6 | frege6 38624 |
| [Frege1879] p. 34 | Proposition 7 | frege7 38626 |
| [Frege1879] p. 35 | Axiom 8 | ax-frege8 38627 axfrege8 38625 |
| [Frege1879] p. 35 | Proposition 8 | pm2.04 90 wl-pm2.04 33605 |
| [Frege1879] p. 35 | Proposition 9 | frege9 38630 |
| [Frege1879] p. 36 | Proposition 10 | frege10 38638 |
| [Frege1879] p. 36 | Proposition 11 | frege11 38632 |
| [Frege1879] p. 37 | Proposition 12 | frege12 38631 |
| [Frege1879] p. 37 | Proposition 13 | frege13 38640 |
| [Frege1879] p. 37 | Proposition 14 | frege14 38641 |
| [Frege1879] p. 38 | Proposition 15 | frege15 38644 |
| [Frege1879] p. 38 | Proposition 16 | frege16 38634 |
| [Frege1879] p. 39 | Proposition 17 | frege17 38639 |
| [Frege1879] p. 39 | Proposition 18 | frege18 38636 |
| [Frege1879] p. 39 | Proposition 19 | frege19 38642 |
| [Frege1879] p. 40 | Proposition 20 | frege20 38646 |
| [Frege1879] p. 40 | Proposition 21 | frege21 38645 |
| [Frege1879] p. 41 | Proposition 22 | frege22 38637 |
| [Frege1879] p. 42 | Proposition 23 | frege23 38643 |
| [Frege1879] p. 42 | Proposition 24 | frege24 38633 |
| [Frege1879] p. 42 | Proposition 25 | frege25 38635 rp-frege25 38623 |
| [Frege1879] p. 42 | Proposition 26 | frege26 38628 |
| [Frege1879] p. 43 | Axiom 28 | ax-frege28 38648 |
| [Frege1879] p. 43 | Proposition 27 | frege27 38629 |
| [Frege1879] p. 43 | Proposition 28 | con3 150 |
| [Frege1879] p. 43 | Proposition 29 | frege29 38649 |
| [Frege1879] p. 44 | Axiom 31 | ax-frege31 38652 axfrege31 38651 |
| [Frege1879] p. 44 | Proposition 30 | frege30 38650 |
| [Frege1879] p. 44 | Proposition 31 | notnotr 128 |
| [Frege1879] p. 44 | Proposition 32 | frege32 38653 |
| [Frege1879] p. 44 | Proposition 33 | frege33 38654 |
| [Frege1879] p. 45 | Proposition 34 | frege34 38655 |
| [Frege1879] p. 45 | Proposition 35 | frege35 38656 |
| [Frege1879] p. 45 | Proposition 36 | frege36 38657 |
| [Frege1879] p. 46 | Proposition 37 | frege37 38658 |
| [Frege1879] p. 46 | Proposition 38 | frege38 38659 |
| [Frege1879] p. 46 | Proposition 39 | frege39 38660 |
| [Frege1879] p. 46 | Proposition 40 | frege40 38661 |
| [Frege1879] p. 47 | Axiom 41 | ax-frege41 38663 axfrege41 38662 |
| [Frege1879] p. 47 | Proposition 41 | notnot 138 |
| [Frege1879] p. 47 | Proposition 42 | frege42 38664 |
| [Frege1879] p. 47 | Proposition 43 | frege43 38665 |
| [Frege1879] p. 47 | Proposition 44 | frege44 38666 |
| [Frege1879] p. 47 | Proposition 45 | frege45 38667 |
| [Frege1879] p. 48 | Proposition 46 | frege46 38668 |
| [Frege1879] p. 48 | Proposition 47 | frege47 38669 |
| [Frege1879] p. 49 | Proposition 48 | frege48 38670 |
| [Frege1879] p. 49 | Proposition 49 | frege49 38671 |
| [Frege1879] p. 49 | Proposition 50 | frege50 38672 |
| [Frege1879] p. 50 | Axiom 52 | ax-frege52a 38675 ax-frege52c 38706 frege52aid 38676 frege52b 38707 |
| [Frege1879] p. 50 | Axiom 54 | ax-frege54a 38680 ax-frege54c 38710 frege54b 38711 |
| [Frege1879] p. 50 | Proposition 51 | frege51 38673 |
| [Frege1879] p. 50 | Proposition 52 | dfsbcq 3589 |
| [Frege1879] p. 50 | Proposition 53 | frege53a 38678 frege53aid 38677 frege53b 38708 frege53c 38732 |
| [Frege1879] p. 50 | Proposition 54 | biid 251 eqid 2771 |
| [Frege1879] p. 50 | Proposition 55 | frege55a 38686 frege55aid 38683 frege55b 38715 frege55c 38736 frege55cor1a 38687 frege55lem2a 38685 frege55lem2b 38714 frege55lem2c 38735 |
| [Frege1879] p. 50 | Proposition 56 | frege56a 38689 frege56aid 38688 frege56b 38716 frege56c 38737 |
| [Frege1879] p. 51 | Axiom 58 | ax-frege58a 38693 ax-frege58b 38719 frege58bid 38720 frege58c 38739 |
| [Frege1879] p. 51 | Proposition 57 | frege57a 38691 frege57aid 38690 frege57b 38717 frege57c 38738 |
| [Frege1879] p. 51 | Proposition 58 | spsbc 3600 |
| [Frege1879] p. 51 | Proposition 59 | frege59a 38695 frege59b 38722 frege59c 38740 |
| [Frege1879] p. 52 | Proposition 60 | frege60a 38696 frege60b 38723 frege60c 38741 |
| [Frege1879] p. 52 | Proposition 61 | frege61a 38697 frege61b 38724 frege61c 38742 |
| [Frege1879] p. 52 | Proposition 62 | frege62a 38698 frege62b 38725 frege62c 38743 |
| [Frege1879] p. 52 | Proposition 63 | frege63a 38699 frege63b 38726 frege63c 38744 |
| [Frege1879] p. 53 | Proposition 64 | frege64a 38700 frege64b 38727 frege64c 38745 |
| [Frege1879] p. 53 | Proposition 65 | frege65a 38701 frege65b 38728 frege65c 38746 |
| [Frege1879] p. 54 | Proposition 66 | frege66a 38702 frege66b 38729 frege66c 38747 |
| [Frege1879] p. 54 | Proposition 67 | frege67a 38703 frege67b 38730 frege67c 38748 |
| [Frege1879] p. 54 | Proposition 68 | frege68a 38704 frege68b 38731 frege68c 38749 |
| [Frege1879] p. 55 | Definition 69 | dffrege69 38750 |
| [Frege1879] p. 58 | Proposition 70 | frege70 38751 |
| [Frege1879] p. 59 | Proposition 71 | frege71 38752 |
| [Frege1879] p. 59 | Proposition 72 | frege72 38753 |
| [Frege1879] p. 59 | Proposition 73 | frege73 38754 |
| [Frege1879] p. 60 | Definition 76 | dffrege76 38757 |
| [Frege1879] p. 60 | Proposition 74 | frege74 38755 |
| [Frege1879] p. 60 | Proposition 75 | frege75 38756 |
| [Frege1879] p. 62 | Proposition 77 | frege77 38758 frege77d 38562 |
| [Frege1879] p. 63 | Proposition 78 | frege78 38759 |
| [Frege1879] p. 63 | Proposition 79 | frege79 38760 |
| [Frege1879] p. 63 | Proposition 80 | frege80 38761 |
| [Frege1879] p. 63 | Proposition 81 | frege81 38762 frege81d 38563 |
| [Frege1879] p. 64 | Proposition 82 | frege82 38763 |
| [Frege1879] p. 65 | Proposition 83 | frege83 38764 frege83d 38564 |
| [Frege1879] p. 65 | Proposition 84 | frege84 38765 |
| [Frege1879] p. 66 | Proposition 85 | frege85 38766 |
| [Frege1879] p. 66 | Proposition 86 | frege86 38767 |
| [Frege1879] p. 66 | Proposition 87 | frege87 38768 frege87d 38566 |
| [Frege1879] p. 67 | Proposition 88 | frege88 38769 |
| [Frege1879] p. 68 | Proposition 89 | frege89 38770 |
| [Frege1879] p. 68 | Proposition 90 | frege90 38771 |
| [Frege1879] p. 68 | Proposition 91 | frege91 38772 frege91d 38567 |
| [Frege1879] p. 69 | Proposition 92 | frege92 38773 |
| [Frege1879] p. 70 | Proposition 93 | frege93 38774 |
| [Frege1879] p. 70 | Proposition 94 | frege94 38775 |
| [Frege1879] p. 70 | Proposition 95 | frege95 38776 |
| [Frege1879] p. 71 | Definition 99 | dffrege99 38780 |
| [Frege1879] p. 71 | Proposition 96 | frege96 38777 frege96d 38565 |
| [Frege1879] p. 71 | Proposition 97 | frege97 38778 frege97d 38568 |
| [Frege1879] p. 71 | Proposition 98 | frege98 38779 frege98d 38569 |
| [Frege1879] p. 72 | Proposition 100 | frege100 38781 |
| [Frege1879] p. 72 | Proposition 101 | frege101 38782 |
| [Frege1879] p. 72 | Proposition 102 | frege102 38783 frege102d 38570 |
| [Frege1879] p. 73 | Proposition 103 | frege103 38784 |
| [Frege1879] p. 73 | Proposition 104 | frege104 38785 |
| [Frege1879] p. 73 | Proposition 105 | frege105 38786 |
| [Frege1879] p. 73 | Proposition 106 | frege106 38787 frege106d 38571 |
| [Frege1879] p. 74 | Proposition 107 | frege107 38788 |
| [Frege1879] p. 74 | Proposition 108 | frege108 38789 frege108d 38572 |
| [Frege1879] p. 74 | Proposition 109 | frege109 38790 frege109d 38573 |
| [Frege1879] p. 75 | Proposition 110 | frege110 38791 |
| [Frege1879] p. 75 | Proposition 111 | frege111 38792 frege111d 38575 |
| [Frege1879] p. 76 | Proposition 112 | frege112 38793 |
| [Frege1879] p. 76 | Proposition 113 | frege113 38794 |
| [Frege1879] p. 76 | Proposition 114 | frege114 38795 frege114d 38574 |
| [Frege1879] p. 77 | Definition 115 | dffrege115 38796 |
| [Frege1879] p. 77 | Proposition 116 | frege116 38797 |
| [Frege1879] p. 78 | Proposition 117 | frege117 38798 |
| [Frege1879] p. 78 | Proposition 118 | frege118 38799 |
| [Frege1879] p. 78 | Proposition 119 | frege119 38800 |
| [Frege1879] p. 78 | Proposition 120 | frege120 38801 |
| [Frege1879] p. 79 | Proposition 121 | frege121 38802 |
| [Frege1879] p. 79 | Proposition 122 | frege122 38803 frege122d 38576 |
| [Frege1879] p. 79 | Proposition 123 | frege123 38804 |
| [Frege1879] p. 80 | Proposition 124 | frege124 38805 frege124d 38577 |
| [Frege1879] p. 81 | Proposition 125 | frege125 38806 |
| [Frege1879] p. 81 | Proposition 126 | frege126 38807 frege126d 38578 |
| [Frege1879] p. 82 | Proposition 127 | frege127 38808 |
| [Frege1879] p. 83 | Proposition 128 | frege128 38809 |
| [Frege1879] p. 83 | Proposition 129 | frege129 38810 frege129d 38579 |
| [Frege1879] p. 84 | Proposition 130 | frege130 38811 |
| [Frege1879] p. 85 | Proposition 131 | frege131 38812 frege131d 38580 |
| [Frege1879] p. 86 | Proposition 132 | frege132 38813 |
| [Frege1879] p. 86 | Proposition 133 | frege133 38814 frege133d 38581 |
| [Fremlin1] p. 13 | Definition 111G (b) | df-salgen 41045 |
| [Fremlin1] p. 13 | Definition 111G (d) | borelmbl 41365 |
| [Fremlin1] p. 13 | Proposition 111G (b) | salgenss 41066 |
| [Fremlin1] p. 14 | Definition 112A | ismea 41180 |
| [Fremlin1] p. 15 | Remark 112B (d) | psmeasure 41200 |
| [Fremlin1] p. 15 | Property 112C (a) | meadjun 41191 meadjunre 41205 |
| [Fremlin1] p. 15 | Property 112C (b) | meassle 41192 |
| [Fremlin1] p. 15 | Property 112C (c) | meaunle 41193 |
| [Fremlin1] p. 16 | Property 112C (d) | iundjiun 41189 meaiunle 41198 meaiunlelem 41197 |
| [Fremlin1] p. 16 | Proposition 112C (e) | meaiuninc 41210 meaiuninc2 41211 meaiuninc3 41214 meaiuninc3v 41213 meaiunincf 41212 meaiuninclem 41209 |
| [Fremlin1] p. 16 | Proposition 112C (f) | meaiininc 41216 meaiininc2 41217 meaiininclem 41215 |
| [Fremlin1] p. 19 | Theorem 113C | caragen0 41235 caragendifcl 41243 caratheodory 41257 omelesplit 41247 |
| [Fremlin1] p. 19 | Definition 113A | isome 41223 isomennd 41260 isomenndlem 41259 |
| [Fremlin1] p. 19 | Remark 113B (c) | omeunle 41245 |
| [Fremlin1] p. 19 | Definition 112Df | caragencmpl 41264 voncmpl 41350 |
| [Fremlin1] p. 19 | Definition 113A (ii) | omessle 41227 |
| [Fremlin1] p. 20 | Theorem 113C | carageniuncl 41252 carageniuncllem1 41250 carageniuncllem2 41251 caragenuncl 41242 caragenuncllem 41241 caragenunicl 41253 |
| [Fremlin1] p. 21 | Remark 113D | caragenel2d 41261 |
| [Fremlin1] p. 21 | Theorem 113C | caratheodorylem1 41255 caratheodorylem2 41256 |
| [Fremlin1] p. 21 | Exercise 113Xa | caragencmpl 41264 |
| [Fremlin1] p. 23 | Lemma 114B | hoidmv1le 41323 hoidmv1lelem1 41320 hoidmv1lelem2 41321 hoidmv1lelem3 41322 |
| [Fremlin1] p. 25 | Definition 114E | isvonmbl 41367 |
| [Fremlin1] p. 29 | Lemma 115B | hoidmv1le 41323 hoidmvle 41329 hoidmvlelem1 41324 hoidmvlelem2 41325 hoidmvlelem3 41326 hoidmvlelem4 41327 hoidmvlelem5 41328 hsphoidmvle2 41314 hsphoif 41305 hsphoival 41308 |
| [Fremlin1] p. 29 | Definition 1135 (b) | hoicvr 41277 |
| [Fremlin1] p. 29 | Definition 115A (b) | hoicvrrex 41285 |
| [Fremlin1] p. 29 | Definition 115A (c) | hoidmv0val 41312 hoidmvn0val 41313 hoidmvval 41306 hoidmvval0 41316 hoidmvval0b 41319 |
| [Fremlin1] p. 30 | Lemma 115B | hoiprodp1 41317 hsphoidmvle 41315 |
| [Fremlin1] p. 30 | Definition 115C | df-ovoln 41266 df-voln 41268 |
| [Fremlin1] p. 30 | Proposition 115D (a) | dmovn 41333 ovn0 41295 ovn0lem 41294 ovnf 41292 ovnome 41302 ovnssle 41290 ovnsslelem 41289 ovnsupge0 41286 |
| [Fremlin1] p. 30 | Proposition 115D (b) | ovnhoi 41332 ovnhoilem1 41330 ovnhoilem2 41331 vonhoi 41396 |
| [Fremlin1] p. 31 | Lemma 115F | hoidifhspdmvle 41349 hoidifhspf 41347 hoidifhspval 41337 hoidifhspval2 41344 hoidifhspval3 41348 hspmbl 41358 hspmbllem1 41355 hspmbllem2 41356 hspmbllem3 41357 |
| [Fremlin1] p. 31 | Definition 115E | voncmpl 41350 vonmea 41303 |
| [Fremlin1] p. 31 | Proposition 115D (a)(iv) | ovnsubadd 41301 ovnsubadd2 41375 ovnsubadd2lem 41374 ovnsubaddlem1 41299 ovnsubaddlem2 41300 |
| [Fremlin1] p. 32 | Proposition 115G (a) | hoimbl 41360 hoimbl2 41394 hoimbllem 41359 hspdifhsp 41345 opnvonmbl 41363 opnvonmbllem2 41362 |
| [Fremlin1] p. 32 | Proposition 115G (b) | borelmbl 41365 |
| [Fremlin1] p. 32 | Proposition 115G (c) | iccvonmbl 41408 iccvonmbllem 41407 ioovonmbl 41406 |
| [Fremlin1] p. 32 | Proposition 115G (d) | vonicc 41414 vonicclem2 41413 vonioo 41411 vonioolem2 41410 vonn0icc 41417 vonn0icc2 41421 vonn0ioo 41416 vonn0ioo2 41419 |
| [Fremlin1] p. 32 | Proposition 115G (e) | ctvonmbl 41418 snvonmbl 41415 vonct 41422 vonsn 41420 |
| [Fremlin1] p. 35 | Lemma 121A | subsalsal 41089 |
| [Fremlin1] p. 35 | Lemma 121A (iii) | subsaliuncl 41088 subsaliuncllem 41087 |
| [Fremlin1] p. 35 | Proposition 121B | salpreimagtge 41449 salpreimalegt 41435 salpreimaltle 41450 |
| [Fremlin1] p. 35 | Proposition 121B (i) | issmf 41452 issmff 41458 issmflem 41451 |
| [Fremlin1] p. 35 | Proposition 121B (ii) | issmfle 41469 issmflelem 41468 smfpreimale 41478 |
| [Fremlin1] p. 35 | Proposition 121B (iii) | issmfgt 41480 issmfgtlem 41479 |
| [Fremlin1] p. 36 | Definition 121C | df-smblfn 41425 issmf 41452 issmff 41458 issmfge 41493 issmfgelem 41492 issmfgt 41480 issmfgtlem 41479 issmfle 41469 issmflelem 41468 issmflem 41451 |
| [Fremlin1] p. 36 | Proposition 121B | salpreimagelt 41433 salpreimagtlt 41454 salpreimalelt 41453 |
| [Fremlin1] p. 36 | Proposition 121B (iv) | issmfge 41493 issmfgelem 41492 |
| [Fremlin1] p. 36 | Proposition 121D (a) | bormflebmf 41477 |
| [Fremlin1] p. 36 | Proposition 121D (b) | cnfrrnsmf 41475 cnfsmf 41464 |
| [Fremlin1] p. 36 | Proposition 121D (c) | decsmf 41490 decsmflem 41489 incsmf 41466 incsmflem 41465 |
| [Fremlin1] p. 37 | Proposition 121E (a) | pimconstlt0 41429 pimconstlt1 41430 smfconst 41473 |
| [Fremlin1] p. 37 | Proposition 121E (b) | smfadd 41488 smfaddlem1 41486 smfaddlem2 41487 |
| [Fremlin1] p. 37 | Proposition 121E (c) | smfmulc1 41518 |
| [Fremlin1] p. 37 | Proposition 121E (d) | smfmul 41517 smfmullem1 41513 smfmullem2 41514 smfmullem3 41515 smfmullem4 41516 |
| [Fremlin1] p. 37 | Proposition 121E (e) | smfdiv 41519 |
| [Fremlin1] p. 37 | Proposition 121E (f) | smfpimbor1 41522 smfpimbor1lem2 41521 |
| [Fremlin1] p. 37 | Proposition 121E (g) | smfco 41524 |
| [Fremlin1] p. 37 | Proposition 121E (h) | smfres 41512 |
| [Fremlin1] p. 38 | Proposition 121E (e) | smfrec 41511 |
| [Fremlin1] p. 38 | Proposition 121E (f) | smfpimbor1lem1 41520 smfresal 41510 |
| [Fremlin1] p. 38 | Proposition 121F (a) | smflim 41500 smflim2 41527 smflimlem1 41494 smflimlem2 41495 smflimlem3 41496 smflimlem4 41497 smflimlem5 41498 smflimlem6 41499 smflimmpt 41531 |
| [Fremlin1] p. 38 | Proposition 121F (b) | smfsup 41535 smfsuplem1 41532 smfsuplem2 41533 smfsuplem3 41534 smfsupmpt 41536 smfsupxr 41537 |
| [Fremlin1] p. 38 | Proposition 121F (c) | smfinf 41539 smfinflem 41538 smfinfmpt 41540 |
| [Fremlin1] p. 39 | Remark 121G | smflim 41500 smflim2 41527 smflimmpt 41531 |
| [Fremlin1] p. 39 | Proposition 121F | smfpimcc 41529 |
| [Fremlin1] p. 39 | Proposition 121F (d) | smflimsup 41549 smflimsuplem2 41542 smflimsuplem6 41546 smflimsuplem7 41547 smflimsuplem8 41548 smflimsupmpt 41550 |
| [Fremlin1] p. 39 | Proposition 121F (e) | smfliminf 41552 smfliminflem 41551 smfliminfmpt 41553 |
| [Fremlin1] p. 80 | Definition 135E (b) | df-smblfn 41425 |
| [Fremlin5] p. 193 | Proposition 563Gb | nulmbl2 23524 |
| [Fremlin5] p. 213 | Lemma 565Ca | uniioovol 23567 |
| [Fremlin5] p. 214 | Lemma 565Ca | uniioombl 23577 |
| [Fremlin5] p. 218 | Lemma 565Ib | ftc1anclem6 33821 |
| [Fremlin5] p. 220 | Theorem 565Ma | ftc1anc 33824 |
| [FreydScedrov] p. 283 | Axiom of Infinity | ax-inf 8703 inf1 8687 inf2 8688 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 9939 enqer 9949 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nq 9944 df-nq 9940 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 9936 df-plq 9942 |
| [Gleason] p. 119 | Proposition 9-2.4 | caovmo 7022 df-mpq 9937 df-mq 9943 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 9945 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnq 10003 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 10004 ltbtwnnq 10006 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanq 9999 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnq 10000 |
| [Gleason] p. 120 | Proposition 9-2.6(iv) | ltrnq 10007 |
| [Gleason] p. 121 | Definition 9-3.1 | df-np 10009 |
| [Gleason] p. 121 | Definition 9-3.1 (ii) | prcdnq 10021 |
| [Gleason] p. 121 | Definition 9-3.1(iii) | prnmax 10023 |
| [Gleason] p. 122 | Definition | df-1p 10010 |
| [Gleason] p. 122 | Remark (1) | prub 10022 |
| [Gleason] p. 122 | Lemma 9-3.4 | prlem934 10061 |
| [Gleason] p. 122 | Proposition 9-3.2 | df-ltp 10013 |
| [Gleason] p. 122 | Proposition 9-3.3 | ltsopr 10060 psslinpr 10059 supexpr 10082 suplem1pr 10080 suplem2pr 10081 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 10046 addclprlem1 10044 addclprlem2 10045 df-plp 10011 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addasspr 10050 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcompr 10049 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 10062 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 10071 ltexprlem1 10064 ltexprlem2 10065 ltexprlem3 10066 ltexprlem4 10067 ltexprlem5 10068 ltexprlem6 10069 ltexprlem7 10070 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltapr 10073 ltaprlem 10072 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanpr 10074 |
| [Gleason] p. 124 | Lemma 9-3.6 | prlem936 10075 |
| [Gleason] p. 124 | Proposition 9-3.7 | df-mp 10012 mulclpr 10048 mulclprlem 10047 reclem2pr 10076 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 10057 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulasspr 10052 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcompr 10051 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrpr 10056 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 10079 reclem3pr 10077 reclem4pr 10078 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 10083 enrer 10092 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 10088 df-1r 10089 df-nr 10084 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 10086 df-plr 10085 negexsr 10129 recexsr 10134 recexsrlem 10130 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 10087 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 11221 creur 11220 cru 11218 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 10215 axcnre 10191 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 14063 crimd 14180 crimi 14141 crre 14062 crred 14179 crrei 14140 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 14065 remimd 14146 |
| [Gleason] p. 133 | Definition 10.36 | absval2 14232 absval2d 14392 absval2i 14344 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 14089 cjaddd 14168 cjaddi 14136 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 14090 cjmuld 14169 cjmuli 14137 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 14088 cjcjd 14147 cjcji 14119 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 14087 cjreb 14071 cjrebd 14150 cjrebi 14122 cjred 14174 rere 14070 rereb 14068 rerebd 14149 rerebi 14121 rered 14172 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 14096 addcjd 14160 addcji 14131 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 14186 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 14227 abscjd 14397 abscji 14348 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 14237 abs00d 14393 abs00i 14345 absne0d 14394 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 14269 releabsd 14398 releabsi 14349 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 14242 absmuld 14401 absmuli 14351 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 14230 sqabsaddi 14352 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 14278 abstrid 14403 abstrii 14355 |
| [Gleason] p. 134 | Definition 10-4.1 | 0exp0e1 13072 df-exp 13068 exp0 13071 expp1 13074 expp1d 13216 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | cxpadd 24646 cxpaddd 24684 expadd 13109 expaddd 13217 expaddz 13111 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 24655 cxpmuld 24701 expmul 13112 expmuld 13218 expmulz 13113 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulcxp 24652 mulcxpd 24695 mulexp 13106 mulexpd 13230 mulexpz 13107 |
| [Gleason] p. 140 | Exercise 1 | znnen 15147 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 12535 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 14570 rlimadd 14581 rlimdiv 14584 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 14572 rlimsub 14582 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 14571 rlimmul 14583 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 14575 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 14522 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 14542 climcj 14543 climim 14545 climre 14544 rlimabs 14547 rlimcj 14548 rlimim 14550 rlimre 14549 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 10285 df-xr 10284 ltxr 12154 |
| [Gleason] p. 175 | Definition 12-4.1 | df-limsup 14410 limsupval 14413 |
| [Gleason] p. 180 | Theorem 12-5.1 | climsup 14608 |
| [Gleason] p. 180 | Theorem 12-5.3 | caucvg 14617 caucvgb 14618 caucvgr 14614 climcau 14609 |
| [Gleason] p. 182 | Exercise 3 | cvgcmp 14755 |
| [Gleason] p. 182 | Exercise 4 | cvgrat 14822 |
| [Gleason] p. 195 | Theorem 13-2.12 | abs1m 14283 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 12837 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 19955 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 22368 xmet0 22367 |
| [Gleason] p. 223 | Definition 14-1.1(b) | metgt0 22384 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 22375 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 22377 mstri 22494 xmettri 22376 xmstri 22493 |
| [Gleason] p. 225 | Definition 14-1.5 | xpsmet 22407 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 21672 |
| [Gleason] p. 240 | Theorem 14-4.3 | metcnp4 23327 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 22565 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn 22888 addcn2 14532 mulcn 22890 mulcn2 14534 subcn 22889 subcn2 14533 |
| [Gleason] p. 295 | Remark | bcval3 13297 bcval4 13298 |
| [Gleason] p. 295 | Equation 2 | bcpasc 13312 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 13295 df-bc 13294 |
| [Gleason] p. 296 | Remark | bcn0 13301 bcnn 13303 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 14769 |
| [Gleason] p. 308 | Equation 2 | ef0 15027 |
| [Gleason] p. 308 | Equation 3 | efcj 15028 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 15033 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 15037 |
| [Gleason] p. 310 | Equation 14 | sinadd 15100 |
| [Gleason] p. 310 | Equation 15 | cosadd 15101 |
| [Gleason] p. 311 | Equation 17 | sincossq 15112 |
| [Gleason] p. 311 | Equation 18 | cosbnd 15117 sinbnd 15116 |
| [Gleason] p. 311 | Lemma 15-4.7 | sqeqor 13185 sqeqori 13183 |
| [Gleason] p. 311 | Definition of pi | df-pi 15009 |
| [Godowski] p. 730 | Equation SF | goeqi 29472 |
| [GodowskiGreechie] p. 249 | Equation IV | 3oai 28867 |
| [Golan] p. 1 | Remark | srgisid 18736 |
| [Golan] p. 1 | Definition | df-srg 18714 |
| [Golan] p. 149 | Definition | df-slmd 30094 |
| [GramKnuthPat], p. 47 | Definition 2.42 | df-fwddif 32603 |
| [Gratzer] p. 23 | Section 0.6 | df-mre 16454 |
| [Gratzer] p. 27 | Section 0.6 | df-mri 16456 |
| [Hall] p. 1 | Section 1.1 | df-asslaw 42347 df-cllaw 42345 df-comlaw 42346 |
| [Hall] p. 2 | Section 1.2 | df-clintop 42359 |
| [Hall] p. 7 | Section 1.3 | df-sgrp2 42380 |
| [Halmos] p. 31 | Theorem 17.3 | riesz1 29264 riesz2 29265 |
| [Halmos] p. 41 | Definition of Hermitian | hmopadj2 29140 |
| [Halmos] p. 42 | Definition of projector ordering | pjordi 29372 |
| [Halmos] p. 43 | Theorem 26.1 | elpjhmop 29384 elpjidm 29383 pjnmopi 29347 |
| [Halmos] p. 44 | Remark | pjinormi 28886 pjinormii 28875 |
| [Halmos] p. 44 | Theorem 26.2 | elpjch 29388 pjrn 28906 pjrni 28901 pjvec 28895 |
| [Halmos] p. 44 | Theorem 26.3 | pjnorm2 28926 |
| [Halmos] p. 44 | Theorem 26.4 | hmopidmpj 29353 hmopidmpji 29351 |
| [Halmos] p. 45 | Theorem 27.1 | pjinvari 29390 |
| [Halmos] p. 45 | Theorem 27.3 | pjoci 29379 pjocvec 28896 |
| [Halmos] p. 45 | Theorem 27.4 | pjorthcoi 29368 |
| [Halmos] p. 48 | Theorem 29.2 | pjssposi 29371 |
| [Halmos] p. 48 | Theorem 29.3 | pjssdif1i 29374 pjssdif2i 29373 |
| [Halmos] p. 50 | Definition of spectrum | df-spec 29054 |
| [Hamilton] p. 28 | Definition 2.1 | ax-1 6 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 23 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1870 |
| [Hatcher] p. 25 | Definition | df-phtpc 23011 df-phtpy 22990 |
| [Hatcher] p. 26 | Definition | df-pco 23024 df-pi1 23027 |
| [Hatcher] p. 26 | Proposition 1.2 | phtpcer 23014 |
| [Hatcher] p. 26 | Proposition 1.3 | pi1grp 23069 |
| [Hefferon] p. 240 | Definition 3.12 | df-dmat 20514 df-dmatalt 42710 |
| [Helfgott] p. 2 | Theorem | tgoldbach 42228 |
| [Helfgott] p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 42213 |
| [Helfgott] p. 4 | Section 1.2.2 | ax-hgprmladder 42225 bgoldbtbnd 42220 bgoldbtbnd 42220 tgblthelfgott 42226 |
| [Helfgott] p. 5 | Proposition 1.1 | circlevma 31060 |
| [Helfgott] p. 69 | Statement 7.49 | circlemethhgt 31061 |
| [Helfgott] p. 69 | Statement 7.50 | hgt750lema 31075 hgt750lemb 31074 hgt750leme 31076 hgt750lemf 31071 hgt750lemg 31072 |
| [Helfgott] p. 70 | Section 7.4 | ax-tgoldbachgt 42222 tgoldbachgt 31081 tgoldbachgtALTV 42223 tgoldbachgtd 31080 |
| [Helfgott] p. 70 | Statement 7.49 | ax-hgt749 31062 |
| [Herstein] p. 54 | Exercise 28 | df-grpo 27687 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 17641 grpoideu 27703 mndideu 17512 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 17664 grpoinveu 27713 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 17690 grpo2inv 27725 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 17701 grpoinvop 27727 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3e 17723 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1841 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1842 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1844 |
| [Holland] p. 1519 | Theorem 2 | sumdmdi 29619 |
| [Holland] p. 1520 | Lemma 5 | cdj1i 29632 cdj3i 29640 cdj3lem1 29633 cdjreui 29631 |
| [Holland] p. 1524 | Lemma 7 | mddmdin0i 29630 |
| [Holland95] p. 13 | Theorem 3.6 | hlathil 37769 |
| [Holland95] p. 14 | Line 15 | hgmapvs 37699 |
| [Holland95] p. 14 | Line 16 | hdmaplkr 37721 |
| [Holland95] p. 14 | Line 17 | hdmapellkr 37722 |
| [Holland95] p. 14 | Line 19 | hdmapglnm2 37719 |
| [Holland95] p. 14 | Line 20 | hdmapip0com 37725 |
| [Holland95] p. 14 | Theorem 3.6 | hdmapevec2 37644 |
| [Holland95] p. 14 | Lines 24 and 25 | hdmapoc 37739 |
| [Holland95] p. 204 | Definition of involution | df-srng 19056 |
| [Holland95] p. 212 | Definition of subspace | df-psubsp 35310 |
| [Holland95] p. 214 | Lemma 3.3 | lclkrlem2v 37336 |
| [Holland95] p. 214 | Definition 3.2 | df-lpolN 37289 |
| [Holland95] p. 214 | Definition of nonsingular | pnonsingN 35740 |
| [Holland95] p. 215 | Lemma 3.3(1) | dihoml4 37185 poml4N 35760 |
| [Holland95] p. 215 | Lemma 3.3(2) | dochexmid 37276 pexmidALTN 35785 pexmidN 35776 |
| [Holland95] p. 218 | Theorem 3.6 | lclkr 37341 |
| [Holland95] p. 218 | Definition of dual vector space | df-ldual 34931 ldualset 34932 |
| [Holland95] p. 222 | Item 1 | df-lines 35308 df-pointsN 35309 |
| [Holland95] p. 222 | Item 2 | df-polarityN 35710 |
| [Holland95] p. 223 | Remark | ispsubcl2N 35754 omllaw4 35053 pol1N 35717 polcon3N 35724 |
| [Holland95] p. 223 | Definition | df-psubclN 35742 |
| [Holland95] p. 223 | Equation for polarity | polval2N 35713 |
| [Holmes] p. 40 | Definition | df-xrn 34473 |
| [Hughes] p. 44 | Equation 1.21b | ax-his3 28281 |
| [Hughes] p. 47 | Definition of projection operator | dfpjop 29381 |
| [Hughes] p. 49 | Equation 1.30 | eighmre 29162 eigre 29034 eigrei 29033 |
| [Hughes] p. 49 | Equation 1.31 | eighmorth 29163 eigorth 29037 eigorthi 29036 |
| [Hughes] p. 137 | Remark (ii) | eigposi 29035 |
| [Huneke] p. 1 | Claim 1 | frgrncvvdeq 27491 |
| [Huneke] p. 1 | Statement 1 | frgrncvvdeqlem7 27487 |
| [Huneke] p. 1 | Statement 2 | frgrncvvdeqlem8 27488 |
| [Huneke] p. 1 | Statement 3 | frgrncvvdeqlem9 27489 |
| [Huneke] p. 2 | Claim 2 | frgrregorufr 27507 frgrregorufr0 27506 frgrregorufrg 27508 |
| [Huneke] p. 2 | Claim 3 | frgrhash2wsp 27514 frrusgrord 27523 frrusgrord0 27522 |
| [Huneke] p. 2 | Statement | df-clwwlknon 27260 |
| [Huneke] p. 2 | Statement 4 | frgrwopreglem4 27497 |
| [Huneke] p. 2 | Statement 5 | frgrwopreg1 27500 frgrwopreg2 27501 frgrwopregasn 27498 frgrwopregbsn 27499 |
| [Huneke] p. 2 | Statement 6 | frgrwopreglem5 27503 |
| [Huneke] p. 2 | Statement 7 | fusgreghash2wspv 27517 |
| [Huneke] p. 2 | Statement 8 | fusgreghash2wsp 27520 |
| [Huneke] p. 2 | Statement 9 | clwlksndivn 27258 numclwlk1 27562 numclwlk1lem1 27560 numclwlk1lem2 27561 numclwwlk1 27548 numclwwlk8 27591 |
| [Huneke] p. 2 | Definition 3 | frgrwopreglem1 27494 |
| [Huneke] p. 2 | Definition 4 | df-clwlks 26902 |
| [Huneke] p. 2 | Definition 6 | 2clwwlk 27531 |
| [Huneke] p. 2 | Definition 7 | numclwwlkovh 27564 numclwwlkovh0 27563 |
| [Huneke] p. 2 | Statement 10 | numclwwlk2 27572 |
| [Huneke] p. 2 | Statement 11 | rusgrnumwlkg 27126 |
| [Huneke] p. 2 | Statement 12 | numclwwlk3 27584 |
| [Huneke] p. 2 | Statement 13 | numclwwlk5 27587 |
| [Huneke] p. 2 | Statement 14 | numclwwlk7 27590 |
| [Indrzejczak] p. 33 | Definition ` `E | natded 27602 natded 27602 |
| [Indrzejczak] p. 33 | Definition ` `I | natded 27602 |
| [Indrzejczak] p. 34 | Definition ` `E | natded 27602 natded 27602 |
| [Indrzejczak] p. 34 | Definition ` `I | natded 27602 |
| [Jech] p. 4 | Definition of class | cv 1630 cvjust 2766 |
| [Jech] p. 42 | Lemma 6.1 | alephexp1 9607 |
| [Jech] p. 42 | Equation 6.1 | alephadd 9605 alephmul 9606 |
| [Jech] p. 43 | Lemma 6.2 | infmap 9604 infmap2 9246 |
| [Jech] p. 71 | Lemma 9.3 | jech9.3 8845 |
| [Jech] p. 72 | Equation 9.3 | scott0 8917 scottex 8916 |
| [Jech] p. 72 | Exercise 9.1 | rankval4 8898 |
| [Jech] p. 72 | Scheme "Collection Principle" | cp 8922 |
| [Jech] p. 78 | Note | opthprc 5306 |
| [JonesMatijasevic] p. 694 | Definition 2.3 | rmxyval 38004 |
| [JonesMatijasevic] p. 695 | Lemma 2.15 | jm2.15nn0 38094 |
| [JonesMatijasevic] p. 695 | Lemma 2.16 | jm2.16nn0 38095 |
| [JonesMatijasevic] p. 695 | Equation 2.7 | rmxadd 38016 |
| [JonesMatijasevic] p. 695 | Equation 2.8 | rmyadd 38020 |
| [JonesMatijasevic] p. 695 | Equation 2.9 | rmxp1 38021 rmyp1 38022 |
| [JonesMatijasevic] p. 695 | Equation 2.10 | rmxm1 38023 rmym1 38024 |
| [JonesMatijasevic] p. 695 | Equation 2.11 | rmx0 38014 rmx1 38015 rmxluc 38025 |
| [JonesMatijasevic] p. 695 | Equation 2.12 | rmy0 38018 rmy1 38019 rmyluc 38026 |
| [JonesMatijasevic] p. 695 | Equation 2.13 | rmxdbl 38028 |
| [JonesMatijasevic] p. 695 | Equation 2.14 | rmydbl 38029 |
| [JonesMatijasevic] p. 696 | Lemma 2.17 | jm2.17a 38051 jm2.17b 38052 jm2.17c 38053 |
| [JonesMatijasevic] p. 696 | Lemma 2.19 | jm2.19 38084 |
| [JonesMatijasevic] p. 696 | Lemma 2.20 | jm2.20nn 38088 |
| [JonesMatijasevic] p. 696 | Theorem 2.18 | jm2.18 38079 |
| [JonesMatijasevic] p. 697 | Lemma 2.24 | jm2.24 38054 jm2.24nn 38050 |
| [JonesMatijasevic] p. 697 | Lemma 2.26 | jm2.26 38093 |
| [JonesMatijasevic] p. 697 | Lemma 2.27 | jm2.27 38099 rmygeid 38055 |
| [JonesMatijasevic] p. 698 | Lemma 3.1 | jm3.1 38111 |
| [Juillerat] p. 11 | Section *5 | etransc 41012 etransclem47 41010 etransclem48 41011 |
| [Juillerat] p. 12 | Equation (7) | etransclem44 41007 |
| [Juillerat] p. 12 | Equation *(7) | etransclem46 41009 |
| [Juillerat] p. 12 | Proof of the derivative calculated | etransclem32 40995 |
| [Juillerat] p. 13 | Proof | etransclem35 40998 |
| [Juillerat] p. 13 | Part of case 2 proven in | etransclem38 41001 |
| [Juillerat] p. 13 | Part of case 2 proven | etransclem24 40987 |
| [Juillerat] p. 13 | Part of case 2: proven in | etransclem41 41004 |
| [Juillerat] p. 14 | Proof | etransclem23 40986 |
| [KalishMontague] p. 81 | Note 1 | ax-6 2057 |
| [KalishMontague] p. 85 | Lemma 2 | equid 2097 |
| [KalishMontague] p. 85 | Lemma 3 | equcomi 2102 |
| [KalishMontague] p. 86 | Lemma 7 | cbvalivw 2092 cbvaliw 2091 |
| [KalishMontague] p. 87 | Lemma 8 | spimvw 2085 spimw 2084 |
| [KalishMontague] p. 87 | Lemma 9 | spfw 2121 spw 2123 |
| [Kalmbach] p. 14 | Definition of lattice | chabs1 28715 chabs1i 28717 chabs2 28716 chabs2i 28718 chjass 28732 chjassi 28685 latabs1 17295 latabs2 17296 |
| [Kalmbach] p. 15 | Definition of atom | df-at 29537 ela 29538 |
| [Kalmbach] p. 15 | Definition of covers | cvbr2 29482 cvrval2 35081 |
| [Kalmbach] p. 16 | Definition | df-ol 34985 df-oml 34986 |
| [Kalmbach] p. 20 | Definition of commutes | cmbr 28783 cmbri 28789 cmtvalN 35018 df-cm 28782 df-cmtN 34984 |
| [Kalmbach] p. 22 | Remark | omllaw5N 35054 pjoml5 28812 pjoml5i 28787 |
| [Kalmbach] p. 22 | Definition | pjoml2 28810 pjoml2i 28784 |
| [Kalmbach] p. 22 | Theorem 2(v) | cmcm 28813 cmcmi 28791 cmcmii 28796 cmtcomN 35056 |
| [Kalmbach] p. 22 | Theorem 2(ii) | omllaw3 35052 omlsi 28603 pjoml 28635 pjomli 28634 |
| [Kalmbach] p. 22 | Definition of OML law | omllaw2N 35051 |
| [Kalmbach] p. 23 | Remark | cmbr2i 28795 cmcm3 28814 cmcm3i 28793 cmcm3ii 28798 cmcm4i 28794 cmt3N 35058 cmt4N 35059 cmtbr2N 35060 |
| [Kalmbach] p. 23 | Lemma 3 | cmbr3 28807 cmbr3i 28799 cmtbr3N 35061 |
| [Kalmbach] p. 25 | Theorem 5 | fh1 28817 fh1i 28820 fh2 28818 fh2i 28821 omlfh1N 35065 |
| [Kalmbach] p. 65 | Remark | chjatom 29556 chslej 28697 chsleji 28657 shslej 28579 shsleji 28569 |
| [Kalmbach] p. 65 | Proposition 1 | chocin 28694 chocini 28653 chsupcl 28539 chsupval2 28609 h0elch 28452 helch 28440 hsupval2 28608 ocin 28495 ococss 28492 shococss 28493 |
| [Kalmbach] p. 65 | Definition of subspace sum | shsval 28511 |
| [Kalmbach] p. 66 | Remark | df-pjh 28594 pjssmi 29364 pjssmii 28880 |
| [Kalmbach] p. 67 | Lemma 3 | osum 28844 osumi 28841 |
| [Kalmbach] p. 67 | Lemma 4 | pjci 29399 |
| [Kalmbach] p. 103 | Exercise 6 | atmd2 29599 |
| [Kalmbach] p. 103 | Exercise 12 | mdsl0 29509 |
| [Kalmbach] p. 140 | Remark | hatomic 29559 hatomici 29558 hatomistici 29561 |
| [Kalmbach] p. 140 | Proposition 1 | atlatmstc 35126 |
| [Kalmbach] p. 140 | Proposition 1(i) | atexch 29580 lsatexch 34850 |
| [Kalmbach] p. 140 | Proposition 1(ii) | chcv1 29554 cvlcvr1 35146 cvr1 35217 |
| [Kalmbach] p. 140 | Proposition 1(iii) | cvexch 29573 cvexchi 29568 cvrexch 35227 |
| [Kalmbach] p. 149 | Remark 2 | chrelati 29563 hlrelat 35209 hlrelat5N 35208 lrelat 34821 |
| [Kalmbach] p. 153 | Exercise 5 | lsmcv 19355 lsmsatcv 34817 spansncv 28852 spansncvi 28851 |
| [Kalmbach] p. 153 | Proposition 1(ii) | lsmcv2 34836 spansncv2 29492 |
| [Kalmbach] p. 266 | Definition | df-st 29410 |
| [Kalmbach2] p. 8 | Definition of adjoint | df-adjh 29048 |
| [KanamoriPincus] p. 415 | Theorem 1.1 | fpwwe 9674 fpwwe2 9671 |
| [KanamoriPincus] p. 416 | Corollary 1.3 | canth4 9675 |
| [KanamoriPincus] p. 417 | Corollary 1.6 | canthp1 9682 |
| [KanamoriPincus] p. 417 | Corollary 1.4(a) | canthnum 9677 |
| [KanamoriPincus] p. 417 | Corollary 1.4(b) | canthwe 9679 |
| [KanamoriPincus] p. 418 | Proposition 1.7 | pwfseq 9692 |
| [KanamoriPincus] p. 419 | Lemma 2.2 | gchcdaidm 9696 gchxpidm 9697 |
| [KanamoriPincus] p. 419 | Theorem 2.1 | gchacg 9708 gchhar 9707 |
| [KanamoriPincus] p. 420 | Lemma 2.3 | pwcdadom 9244 unxpwdom 8654 |
| [KanamoriPincus] p. 421 | Proposition 3.1 | gchpwdom 9698 |
| [Kreyszig] p. 3 | Property M1 | metcl 22357 xmetcl 22356 |
| [Kreyszig] p. 4 | Property M2 | meteq0 22364 |
| [Kreyszig] p. 8 | Definition 1.1-8 | dscmet 22597 |
| [Kreyszig] p. 12 | Equation 5 | conjmul 10948 muleqadd 10877 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 22463 |
| [Kreyszig] p. 19 | Remark | mopntopon 22464 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 22523 mopnm 22469 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 22521 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 22526 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 22567 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 21283 lmmbr 23275 lmmbr2 23276 |
| [Kreyszig] p. 26 | Lemma 1.4-2(a) | lmmo 21405 |
| [Kreyszig] p. 28 | Theorem 1.4-5 | lmcau 23330 |
| [Kreyszig] p. 28 | Definition 1.4-3 | iscau 23293 iscmet2 23311 |
| [Kreyszig] p. 30 | Theorem 1.4-7 | cmetss 23332 |
| [Kreyszig] p. 30 | Theorem 1.4-6(a) | 1stcelcls 21485 metelcls 23322 |
| [Kreyszig] p. 30 | Theorem 1.4-6(b) | metcld 23323 metcld2 23324 |
| [Kreyszig] p. 51 | Equation 2 | clmvneg1 23118 lmodvneg1 19116 nvinv 27834 vcm 27771 |
| [Kreyszig] p. 51 | Equation 1a | clm0vs 23114 lmod0vs 19106 slmd0vs 30117 vc0 27769 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 19107 slmdvs0 30118 vcz 27770 |
| [Kreyszig] p. 58 | Definition 2.2-1 | imsmet 27886 ngpmet 22627 nrmmetd 22599 |
| [Kreyszig] p. 59 | Equation 1 | imsdval 27881 imsdval2 27882 ncvspds 23180 ngpds 22628 |
| [Kreyszig] p. 63 | Problem 1 | nmval 22614 nvnd 27883 |
| [Kreyszig] p. 64 | Problem 2 | nmeq0 22642 nmge0 22641 nvge0 27868 nvz 27864 |
| [Kreyszig] p. 64 | Problem 3 | nmrtri 22648 nvabs 27867 |
| [Kreyszig] p. 91 | Definition 2.7-1 | isblo3i 27996 |
| [Kreyszig] p. 92 | Equation 2 | df-nmoo 27940 |
| [Kreyszig] p. 97 | Theorem 2.7-9(a) | blocn 28002 blocni 28000 |
| [Kreyszig] p. 97 | Theorem 2.7-9(b) | lnocni 28001 |
| [Kreyszig] p. 129 | Definition 3.1-1 | cphipeq0 23223 ipeq0 20200 ipz 27914 |
| [Kreyszig] p. 135 | Problem 2 | pythi 28045 |
| [Kreyszig] p. 137 | Lemma 3-2.1(a) | sii 28049 |
| [Kreyszig] p. 144 | Equation 4 | supcvg 14795 |
| [Kreyszig] p. 144 | Theorem 3.3-1 | minvec 23426 minveco 28080 |
| [Kreyszig] p. 196 | Definition 3.9-1 | df-aj 27945 |
| [Kreyszig] p. 247 | Theorem 4.7-2 | bcth 23345 |
| [Kreyszig] p. 249 | Theorem 4.7-3 | ubth 28069 |
| [Kreyszig] p. 470 | Definition of positive operator ordering | leop 29322 leopg 29321 |
| [Kreyszig] p. 476 | Theorem 9.4-2 | opsqrlem2 29340 |
| [Kreyszig] p. 525 | Theorem 10.1-1 | htth 28115 |
| [Kulpa] p. 547 | Theorem | poimir 33774 |
| [Kulpa] p. 547 | Equation (1) | poimirlem32 33773 |
| [Kulpa] p. 547 | Equation (2) | poimirlem31 33772 |
| [Kulpa] p. 548 | Theorem | broucube 33775 |
| [Kulpa] p. 548 | Equation (6) | poimirlem26 33767 |
| [Kulpa] p. 548 | Equation (7) | poimirlem27 33768 |
| [Kunen] p. 10 | Axiom 0 | ax6e 2412 axnul 4923 |
| [Kunen] p. 11 | Axiom 3 | axnul 4923 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 7285 |
| [Kunen] p. 24 | Definition 10.24 | mapval 8025 mapvalg 8023 |
| [Kunen] p. 30 | Lemma 10.20 | fodom 9550 |
| [Kunen] p. 31 | Definition 10.24 | mapex 8019 |
| [Kunen] p. 95 | Definition 2.1 | df-r1 8795 |
| [Kunen] p. 97 | Lemma 2.10 | r1elss 8837 r1elssi 8836 |
| [Kunen] p. 107 | Exercise 4 | rankop 8889 rankopb 8883 rankuni 8894 rankxplim 8910 rankxpsuc 8913 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4666 |
| [Lang] p. 3 | Definition | df-mnd 17503 |
| [Lang] p. 7 | Definition | dfgrp2e 17656 |
| [Lang] p. 53 | Definition | df-cat 16536 |
| [Lang] p. 54 | Definition | df-iso 16616 |
| [Lang] p. 57 | Definition | df-inito 16848 df-termo 16849 |
| [Lang] p. 58 | Example | irinitoringc 42592 |
| [Lang] p. 58 | Statement | initoeu1 16868 termoeu1 16875 |
| [Lang] p. 62 | Definition | df-func 16725 |
| [Lang] p. 65 | Definition | df-nat 16810 |
| [Lang] p. 91 | Note | df-ringc 42528 |
| [Lang] p. 128 | Remark | dsmmlmod 20306 |
| [Lang] p. 129 | Proof | lincscm 42742 lincscmcl 42744 lincsum 42741 lincsumcl 42743 |
| [Lang] p. 129 | Statement | lincolss 42746 |
| [Lang] p. 129 | Observation | dsmmfi 20299 |
| [Lang] p. 147 | Definition | snlindsntor 42783 |
| [Lang] p. 504 | Statement | mat1 20471 matring 20466 |
| [Lang] p. 504 | Definition | df-mamu 20407 |
| [Lang] p. 505 | Statement | mamuass 20425 mamutpos 20482 matassa 20467 mattposvs 20479 tposmap 20481 |
| [Lang] p. 513 | Definition | mdet1 20625 mdetf 20619 |
| [Lang] p. 513 | Theorem 4.4 | cramer 20717 |
| [Lang] p. 514 | Proposition 4.6 | mdetleib 20611 |
| [Lang] p. 514 | Proposition 4.8 | mdettpos 20635 |
| [Lang] p. 515 | Definition | df-minmar1 20659 smadiadetr 20700 |
| [Lang] p. 515 | Corollary 4.9 | mdetero 20634 mdetralt 20632 |
| [Lang] p. 517 | Proposition 4.15 | mdetmul 20647 |
| [Lang] p. 518 | Definition | df-madu 20658 |
| [Lang] p. 518 | Proposition 4.16 | madulid 20669 madurid 20668 matinv 20702 |
| [Lang] p. 561 | Theorem 3.1 | cayleyhamilton 20915 |
| [Lang], p. 561 | Remark | chpmatply1 20857 |
| [Lang], p. 561 | Definition | df-chpmat 20852 |
| [LarsonHostetlerEdwards] p. 278 | Section 4.1 | dvconstbi 39057 |
| [LarsonHostetlerEdwards] p. 311 | Example 1a | lhe4.4ex1a 39052 |
| [LarsonHostetlerEdwards] p. 375 | Theorem 5.1 | expgrowth 39058 |
| [LeBlanc] p. 277 | Rule R2 | axnul 4923 |
| [Levy] p. 338 | Axiom | df-clab 2758 df-clel 2767 df-cleq 2764 |
| [Levy58] p. 2 | Definition I | isfin1-3 9414 |
| [Levy58] p. 2 | Definition II | df-fin2 9314 |
| [Levy58] p. 2 | Definition Ia | df-fin1a 9313 |
| [Levy58] p. 2 | Definition III | df-fin3 9316 |
| [Levy58] p. 3 | Definition V | df-fin5 9317 |
| [Levy58] p. 3 | Definition IV | df-fin4 9315 |
| [Levy58] p. 4 | Definition VI | df-fin6 9318 |
| [Levy58] p. 4 | Definition VII | df-fin7 9319 |
| [Levy58], p. 3 | Theorem 1 | fin1a2 9443 |
| [Lipparini] p. 3 | Lemma 2.1.1 | nosepssdm 32173 |
| [Lipparini] p. 3 | Lemma 2.1.4 | noresle 32183 |
| [Lipparini] p. 6 | Proposition 4.2 | nosupbnd1 32197 |
| [Lipparini] p. 6 | Proposition 4.3 | nosupbnd2 32199 |
| [Lipparini] p. 7 | Theorem 5.1 | noetalem2 32201 noetalem3 32202 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1841 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1842 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1844 |
| [Maeda] p. 167 | Theorem 1(d) to (e) | mdsymlem6 29607 |
| [Maeda] p. 168 | Lemma 5 | mdsym 29611 mdsymi 29610 |
| [Maeda] p. 168 | Lemma 4(i) | mdsymlem4 29605 mdsymlem6 29607 mdsymlem7 29608 |
| [Maeda] p. 168 | Lemma 4(ii) | mdsymlem8 29609 |
| [MaedaMaeda] p. 1 | Remark | ssdmd1 29512 ssdmd2 29513 ssmd1 29510 ssmd2 29511 |
| [MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 29508 |
| [MaedaMaeda] p. 1 | Definition 1.1 | df-dmd 29480 df-md 29479 mdbr 29493 |
| [MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 29530 mdslj1i 29518 mdslj2i 29519 mdslle1i 29516 mdslle2i 29517 mdslmd1i 29528 mdslmd2i 29529 |
| [MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 29520 mdsl2bi 29522 mdsl2i 29521 |
| [MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 29534 |
| [MaedaMaeda] p. 2 | Lemma 1.5.1 | mdslmd3i 29531 |
| [MaedaMaeda] p. 2 | Lemma 1.5.2 | mdslmd4i 29532 |
| [MaedaMaeda] p. 2 | Lemma 1.5.3 | mdsl0 29509 |
| [MaedaMaeda] p. 2 | Theorem 1.3 | dmdsl3 29514 mdsl3 29515 |
| [MaedaMaeda] p. 3 | Theorem 1.9.1 | csmdsymi 29533 |
| [MaedaMaeda] p. 4 | Theorem 1.14 | mdcompli 29628 |
| [MaedaMaeda] p. 30 | Lemma 7.2 | atlrelat1 35128 hlrelat1 35207 |
| [MaedaMaeda] p. 31 | Lemma 7.5 | lcvexch 34846 |
| [MaedaMaeda] p. 31 | Lemma 7.5.1 | cvmd 29535 cvmdi 29523 cvnbtwn4 29488 cvrnbtwn4 35086 |
| [MaedaMaeda] p. 31 | Lemma 7.5.2 | cvdmd 29536 |
| [MaedaMaeda] p. 31 | Definition 7.4 | cvlcvrp 35147 cvp 29574 cvrp 35223 lcvp 34847 |
| [MaedaMaeda] p. 31 | Theorem 7.6(b) | atmd 29598 |
| [MaedaMaeda] p. 31 | Theorem 7.6(c) | atdmd 29597 |
| [MaedaMaeda] p. 32 | Definition 7.8 | cvlexch4N 35140 hlexch4N 35199 |
| [MaedaMaeda] p. 34 | Exercise 7.1 | atabsi 29600 |
| [MaedaMaeda] p. 41 | Lemma 9.2(delta) | cvrat4 35250 |
| [MaedaMaeda] p. 61 | Definition 15.1 | 0psubN 35556 atpsubN 35560 df-pointsN 35309 pointpsubN 35558 |
| [MaedaMaeda] p. 62 | Theorem 15.5 | df-pmap 35311 pmap11 35569 pmaple 35568 pmapsub 35575 pmapval 35564 |
| [MaedaMaeda] p. 62 | Theorem 15.5.1 | pmap0 35572 pmap1N 35574 |
| [MaedaMaeda] p. 62 | Theorem 15.5.2 | pmapglb 35577 pmapglb2N 35578 pmapglb2xN 35579 pmapglbx 35576 |
| [MaedaMaeda] p. 63 | Equation 15.5.3 | pmapjoin 35659 |
| [MaedaMaeda] p. 67 | Postulate PS1 | ps-1 35284 |
| [MaedaMaeda] p. 68 | Lemma 16.2 | df-padd 35603 paddclN 35649 paddidm 35648 |
| [MaedaMaeda] p. 68 | Condition PS2 | ps-2 35285 |
| [MaedaMaeda] p. 68 | Equation 16.2.1 | paddass 35645 |
| [MaedaMaeda] p. 69 | Lemma 16.4 | ps-1 35284 |
| [MaedaMaeda] p. 69 | Theorem 16.4 | ps-2 35285 |
| [MaedaMaeda] p. 70 | Theorem 16.9 | lsmmod 18295 lsmmod2 18296 lssats 34819 shatomici 29557 shatomistici 29560 shmodi 28589 shmodsi 28588 |
| [MaedaMaeda] p. 130 | Remark 29.6 | dmdmd 29499 mdsymlem7 29608 |
| [MaedaMaeda] p. 132 | Theorem 29.13(e) | pjoml6i 28788 |
| [MaedaMaeda] p. 136 | Lemma 31.1.5 | shjshseli 28692 |
| [MaedaMaeda] p. 139 | Remark | sumdmdii 29614 |
| [Margaris] p. 40 | Rule C | exlimiv 2010 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | ax-3 8 |
| [Margaris] p. 49 | Definition | df-an 383 df-ex 1853 df-or 837 dfbi2 460 |
| [Margaris] p. 51 | Theorem 1 | idALT 23 |
| [Margaris] p. 56 | Theorem 3 | conventions 27599 |
| [Margaris] p. 59 | Section 14 | notnotrALTVD 39671 |
| [Margaris] p. 60 | Theorem 8 | mth8 159 |
| [Margaris] p. 60 | Section 14 | con3ALTVD 39672 |
| [Margaris] p. 79 | Rule C | exinst01 39373 exinst11 39374 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 2061 19.2g 2212 r19.2z 4202 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 2224 rr19.3v 3496 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 2193 |
| [Margaris] p. 89 | Theorem 19.6 | alex 1901 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1854 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 2206 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 2228 19.9h 2283 exlimd 2243 exlimdh 2314 |
| [Margaris] p. 89 | Theorem 19.11 | excom 2198 excomim 2199 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 2326 |
| [Margaris] p. 90 | Section 19 | conventions-label 27600 conventions-label 27600 conventions-label 27600 conventions-label 27600 |
| [Margaris] p. 90 | Theorem 19.14 | exnal 1902 |
| [Margaris] p. 90 | Theorem 19.15 | 2albi 39101 albi 1894 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 2249 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 2250 |
| [Margaris] p. 90 | Theorem 19.18 | 2exbi 39103 exbi 1923 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 2253 |
| [Margaris] p. 90 | Theorem 19.20 | 2alim 39100 2alimdv 1999 alimd 2237 alimdh 1893 alimdv 1997 ax-4 1885 ralimdaa 3107 ralimdv 3112 ralimdva 3111 ralimdvva 3113 sbcimdv 3649 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21 2231 19.21h 2284 19.21t 2229 19.21vv 39099 alrimd 2240 alrimdd 2239 alrimdh 1941 alrimdv 2009 alrimi 2238 alrimih 1899 alrimiv 2007 alrimivv 2008 hbralrimi 3103 r19.21be 3082 r19.21bi 3081 ralrimd 3108 ralrimdv 3117 ralrimdva 3118 ralrimdvv 3122 ralrimdvva 3123 ralrimi 3106 ralrimia 39833 ralrimiv 3114 ralrimiva 3115 ralrimivv 3119 ralrimivva 3120 ralrimivvva 3121 ralrimivw 3116 |
| [Margaris] p. 90 | Theorem 19.22 | 2exim 39102 2eximdv 2000 exim 1909 eximd 2241 eximdh 1942 eximdv 1998 rexim 3156 reximd2a 3161 reximdai 3160 reximdd 39861 reximddv 3166 reximddv2 3168 reximddv3 39860 reximdv 3164 reximdv2 3162 reximdva 3165 reximdvai 3163 reximdvva 3167 reximi2 3158 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 2236 19.23bi 2215 19.23h 2285 exlimdv 2013 exlimdvv 2014 exlimexi 39253 exlimiv 2010 exlimivv 2012 rexlimd3 39852 rexlimdv 3178 rexlimdv3a 3181 rexlimdva 3179 rexlimdva2 39856 rexlimdvaa 3180 rexlimdvv 3185 rexlimdvva 3186 rexlimdvw 3182 rexlimiv 3175 rexlimiva 3176 rexlimivv 3184 |
| [Margaris] p. 90 | Theorem 19.24 | 19.24 2069 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1960 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26 1949 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 2251 r19.27z 4212 r19.27zv 4213 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 2252 19.28vv 39109 r19.28z 4205 r19.28zv 4208 rr19.28v 3497 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1953 r19.29d2r 3228 r19.29imd 3222 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30 1961 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31 2258 19.31vv 39107 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32 2257 r19.32 41682 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33-2 39105 19.33 1964 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 2070 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35 1957 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36 2254 19.36vv 39106 r19.36zv 4214 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37 2256 19.37vv 39108 r19.37zv 4209 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1914 |
| [Margaris] p. 90 | Theorem 19.39 | 19.39 2068 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1966 19.40 1948 r19.40 3236 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 2259 19.41rg 39289 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 2261 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1962 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 2262 r19.44zv 4211 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 2263 r19.45zv 4210 |
| [Margaris] p. 90 | Theorem 1977.23 | 19.23t 2235 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2659 |
| [Mayet] p. 370 | Remark | jpi 29469 largei 29466 stri 29456 |
| [Mayet3] p. 9 | Definition of CH-states | df-hst 29411 ishst 29413 |
| [Mayet3] p. 10 | Theorem | hstrbi 29465 hstri 29464 |
| [Mayet3] p. 1223 | Theorem 4.1 | mayete3i 28927 |
| [Mayet3] p. 1240 | Theorem 7.1 | mayetes3i 28928 |
| [MegPav2000] p. 2344 | Theorem 3.3 | stcltrthi 29477 |
| [MegPav2000] p. 2345 | Definition 3.4-1 | chintcl 28531 chsupcl 28539 |
| [MegPav2000] p. 2345 | Definition 3.4-2 | hatomic 29559 |
| [MegPav2000] p. 2345 | Definition 3.4-3(a) | superpos 29553 |
| [MegPav2000] p. 2345 | Definition 3.4-3(b) | atexch 29580 |
| [MegPav2000] p. 2366 | Figure 7 | pl42N 35790 |
| [MegPav2002] p. 362 | Lemma 2.2 | latj31 17307 latj32 17305 latjass 17303 |
| [Megill] p. 444 | Axiom C5 | ax-5 1991 ax5ALT 34713 |
| [Megill] p. 444 | Section 7 | conventions 27599 |
| [Megill] p. 445 | Lemma L12 | aecom-o 34707 ax-c11n 34694 axc11n 2462 |
| [Megill] p. 446 | Lemma L17 | equtrr 2107 |
| [Megill] p. 446 | Lemma L18 | ax6fromc10 34702 |
| [Megill] p. 446 | Lemma L19 | hbnae-o 34734 hbnae 2469 |
| [Megill] p. 447 | Remark 9.1 | df-sb 2050 sbid 2270 sbidd-misc 42986 sbidd 42985 |
| [Megill] p. 448 | Remark 9.6 | axc14 2519 |
| [Megill] p. 448 | Scheme C4' | ax-c4 34690 |
| [Megill] p. 448 | Scheme C5' | ax-c5 34689 sp 2207 |
| [Megill] p. 448 | Scheme C6' | ax-11 2190 |
| [Megill] p. 448 | Scheme C7' | ax-c7 34691 |
| [Megill] p. 448 | Scheme C8' | ax-7 2093 |
| [Megill] p. 448 | Scheme C9' | ax-c9 34696 |
| [Megill] p. 448 | Scheme C10' | ax-6 2057 ax-c10 34692 |
| [Megill] p. 448 | Scheme C11' | ax-c11 34693 |
| [Megill] p. 448 | Scheme C12' | ax-8 2147 |
| [Megill] p. 448 | Scheme C13' | ax-9 2154 |
| [Megill] p. 448 | Scheme C14' | ax-c14 34697 |
| [Megill] p. 448 | Scheme C15' | ax-c15 34695 |
| [Megill] p. 448 | Scheme C16' | ax-c16 34698 |
| [Megill] p. 448 | Theorem 9.4 | dral1-o 34710 dral1 2475 dral2-o 34736 dral2 2474 drex1 2477 drex2 2478 drsb1 2524 drsb2 2525 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2593 sbequ 2523 sbid2v 2605 |
| [Megill] p. 450 | Example in Appendix | hba1-o 34703 hba1 2315 |
| [Mendelson] p. 35 | Axiom A3 | hirstL-ax3 41574 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 23 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3667 rspsbca 3668 stdpc4 2499 |
| [Mendelson] p. 69 | Axiom 5 | ax-c4 34690 ra4 3674 stdpc5 2232 |
| [Mendelson] p. 81 | Rule C | exlimiv 2010 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 2113 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 2114 |
| [Mendelson] p. 225 | Axiom system NBG | ru 3586 |
| [Mendelson] p. 230 | Exercise 4.8(b) | opthwiener 5108 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 4115 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 4116 |
| [Mendelson] p. 231 | Exercise 4.10(n) | dfin3 4015 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 4064 |
| [Mendelson] p. 231 | Exercise 4.10(q) | dfin4 4016 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddif 3893 |
| [Mendelson] p. 231 | Definition of union | dfun3 4014 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 5048 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 4572 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 5152 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 5153 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssun 5154 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 4595 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 5387 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5799 |
| [Mendelson] p. 244 | Proposition 4.8(g) | epweon 7134 |
| [Mendelson] p. 246 | Definition of successor | df-suc 5871 |
| [Mendelson] p. 250 | Exercise 4.36 | oelim2 7833 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 8283 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 8204 xpsneng 8205 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 8211 xpcomeng 8212 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 8214 |
| [Mendelson] p. 255 | Definition | brsdom 8136 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 8207 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 8017 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 8193 mapsnend 8192 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 8289 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 8288 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 8051 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 8196 |
| [Mendelson] p. 257 | Proposition 4.24(a) | undom 8208 |
| [Mendelson] p. 258 | Exercise 4.56(b) | cdaen 9201 |
| [Mendelson] p. 258 | Exercise 4.56(c) | cdaassen 9210 cdacomen 9209 |
| [Mendelson] p. 258 | Exercise 4.56(f) | cdadom1 9214 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2cda 9208 |
| [Mendelson] p. 258 | Definition of cardinal sum | cdaval 9198 df-cda 9196 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 7769 |
| [Mendelson] p. 266 | Proposition 4.34(f) | oaordex 7796 |
| [Mendelson] p. 275 | Proposition 4.42(d) | entri3 9587 |
| [Mendelson] p. 281 | Definition | df-r1 8795 |
| [Mendelson] p. 281 | Proposition 4.45 (b) to (a) | unir1 8844 |
| [Mendelson] p. 287 | Axiom system MK | ru 3586 |
| [MertziosUnger] p. 152 | Definition | df-frgr 27439 |
| [MertziosUnger] p. 153 | Remark 1 | frgrconngr 27476 |
| [MertziosUnger] p. 153 | Remark 2 | vdgn1frgrv2 27478 vdgn1frgrv3 27479 |
| [MertziosUnger] p. 153 | Remark 3 | vdgfrgrgt2 27480 |
| [MertziosUnger] p. 153 | Proposition 1(a) | n4cyclfrgr 27473 |
| [MertziosUnger] p. 153 | Proposition 1(b) | 2pthfrgr 27466 2pthfrgrrn 27464 2pthfrgrrn2 27465 |
| [Mittelstaedt] p. 9 | Definition | df-oc 28449 |
| [Monk1] p. 22 | Remark | conventions 27599 |
| [Monk1] p. 22 | Theorem 3.1 | conventions 27599 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3983 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 5346 ssrelf 29765 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 5348 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4848 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5794 coi2 5795 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 5476 rn0 5514 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5677 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 5267 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxp 5481 rnxp 5704 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 5338 xp0 5692 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5621 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5618 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 7255 imaexg 7254 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5617 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 6496 funfvop 6474 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 6382 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 6392 |
| [Monk1] p. 43 | Theorem 4.6 | funun 6074 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 6658 dff13f 6659 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 6629 funrnex 7284 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 6651 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5762 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 4628 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 7336 df-1st 7319 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 7337 df-2nd 7320 |
| [Monk1] p. 112 | Theorem 15.17(v) | ranksn 8885 ranksnb 8858 |
| [Monk1] p. 112 | Theorem 15.17(iv) | rankuni2 8886 |
| [Monk1] p. 112 | Theorem 15.17(iii) | rankun 8887 rankunb 8881 |
| [Monk1] p. 113 | Theorem 15.18 | r1val3 8869 |
| [Monk1] p. 113 | Definition 15.19 | df-r1 8795 r1val2 8868 |
| [Monk1] p. 117 | Lemma | zorn2 9534 zorn2g 9531 |
| [Monk1] p. 133 | Theorem 18.11 | cardom 9016 |
| [Monk1] p. 133 | Theorem 18.12 | canth3 9589 |
| [Monk1] p. 133 | Theorem 18.14 | carduni 9011 |
| [Monk2] p. 105 | Axiom C4 | ax-4 1885 |
| [Monk2] p. 105 | Axiom C7 | ax-7 2093 |
| [Monk2] p. 105 | Axiom C8 | ax-12 2203 ax-c15 34695 ax12v2 2205 |
| [Monk2] p. 108 | Lemma 5 | ax-c4 34690 |
| [Monk2] p. 109 | Lemma 12 | ax-11 2190 |
| [Monk2] p. 109 | Lemma 15 | equvini 2492 equvinv 2115 eqvinop 5083 |
| [Monk2] p. 113 | Axiom C5-1 | ax-5 1991 ax5ALT 34713 |
| [Monk2] p. 113 | Axiom C5-2 | ax-10 2174 |
| [Monk2] p. 113 | Axiom C5-3 | ax-11 2190 |
| [Monk2] p. 114 | Lemma 21 | sp 2207 |
| [Monk2] p. 114 | Lemma 22 | axc4 2294 hba1-o 34703 hba1 2315 |
| [Monk2] p. 114 | Lemma 23 | nfia1 2186 |
| [Monk2] p. 114 | Lemma 24 | nfa2 2196 nfra2 3095 |
| [Moore] p. 53 | Part I | df-mre 16454 |
| [Munkres] p. 77 | Example 2 | distop 21020 indistop 21027 indistopon 21026 |
| [Munkres] p. 77 | Example 3 | fctop 21029 fctop2 21030 |
| [Munkres] p. 77 | Example 4 | cctop 21031 |
| [Munkres] p. 78 | Definition of basis | df-bases 20971 isbasis3g 20974 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 16312 tgval2 20981 |
| [Munkres] p. 79 | Remark | tgcl 20994 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 20988 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 21012 tgss3 21011 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 21013 basgen2 21014 |
| [Munkres] p. 83 | Exercise 3 | topdifinf 33533 topdifinfeq 33534 topdifinffin 33532 topdifinfindis 33530 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 21185 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 21063 topcld 21060 |
| [Munkres] p. 93 | Theorem 6.1(2) | iincld 21064 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 21066 |
| [Munkres] p. 94 | Definition of closure | clsval 21062 |
| [Munkres] p. 94 | Definition of interior | ntrval 21061 |
| [Munkres] p. 95 | Theorem 6.5(a) | clsndisj 21100 elcls 21098 |
| [Munkres] p. 95 | Theorem 6.5(b) | elcls3 21108 |
| [Munkres] p. 97 | Theorem 6.6 | clslp 21173 neindisj 21142 |
| [Munkres] p. 97 | Corollary 6.7 | cldlp 21175 |
| [Munkres] p. 97 | Definition of limit point | islp2 21170 lpval 21164 |
| [Munkres] p. 98 | Definition of Hausdorff space | df-haus 21340 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 21252 iscn 21260 iscn2 21263 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 21305 cncnp2 21306 cncnpi 21303 df-cnp 21253 iscnp 21262 iscnp2 21264 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 22568 |
| [Munkres] p. 128 | Theorem 10.3 | metcn4 23328 |
| [Nathanson] p. 123 | Remark | reprgt 31039 reprinfz1 31040 reprlt 31037 |
| [Nathanson] p. 123 | Definition | df-repr 31027 |
| [Nathanson] p. 123 | Chapter 5.1 | circlemethnat 31059 |
| [Nathanson] p. 123 | Proposition | breprexp 31051 breprexpnat 31052 itgexpif 31024 |
| [NielsenChuang] p. 195 | Equation 4.73 | unierri 29303 |
| [OeSilva] p. 2042 | Section 2 | ax-bgbltosilva 42221 |
| [Pfenning] p. 17 | Definition XM | natded 27602 |
| [Pfenning] p. 17 | Definition NNC | natded 27602 notnotrd 130 |
| [Pfenning] p. 17 | Definition ` `C | natded 27602 |
| [Pfenning] p. 18 | Rule" | natded 27602 |
| [Pfenning] p. 18 | Definition /\I | natded 27602 |
| [Pfenning] p. 18 | Definition ` `E | natded 27602 natded 27602 natded 27602 natded 27602 natded 27602 |
| [Pfenning] p. 18 | Definition ` `I | natded 27602 natded 27602 natded 27602 natded 27602 natded 27602 |
| [Pfenning] p. 18 | Definition ` `EL | natded 27602 |
| [Pfenning] p. 18 | Definition ` `ER | natded 27602 |
| [Pfenning] p. 18 | Definition ` `Ea,u | natded 27602 |
| [Pfenning] p. 18 | Definition ` `IR | natded 27602 |
| [Pfenning] p. 18 | Definition ` `Ia | natded 27602 |
| [Pfenning] p. 127 | Definition =E | natded 27602 |
| [Pfenning] p. 127 | Definition =I | natded 27602 |
| [Ponnusamy] p. 361 | Theorem 6.44 | cphip0l 23221 df-dip 27896 dip0l 27913 ip0l 20198 |
| [Ponnusamy] p. 361 | Equation 6.45 | cphipval 23261 ipval 27898 |
| [Ponnusamy] p. 362 | Equation I1 | dipcj 27909 ipcj 20196 |
| [Ponnusamy] p. 362 | Equation I3 | cphdir 23224 dipdir 28037 ipdir 20201 ipdiri 28025 |
| [Ponnusamy] p. 362 | Equation I4 | ipidsq 27905 nmsq 23213 |
| [Ponnusamy] p. 362 | Equation 6.46 | ip0i 28020 |
| [Ponnusamy] p. 362 | Equation 6.47 | ip1i 28022 |
| [Ponnusamy] p. 362 | Equation 6.48 | ip2i 28023 |
| [Ponnusamy] p. 363 | Equation I2 | cphass 23230 dipass 28040 ipass 20207 ipassi 28036 |
| [Prugovecki] p. 186 | Definition of bra | braval 29143 df-bra 29049 |
| [Prugovecki] p. 376 | Equation 8.1 | df-kb 29050 kbval 29153 |
| [PtakPulmannova] p. 66 | Proposition 3.2.17 | atomli 29581 |
| [PtakPulmannova] p. 68 | Lemma 3.1.4 | df-pclN 35695 |
| [PtakPulmannova] p. 68 | Lemma 3.2.20 | atcvat3i 29595 atcvat4i 29596 cvrat3 35249 cvrat4 35250 lsatcvat3 34859 |
| [PtakPulmannova] p. 68 | Definition 3.2.18 | cvbr 29481 cvrval 35076 df-cv 29478 df-lcv 34826 lspsncv0 19360 |
| [PtakPulmannova] p. 72 | Lemma 3.3.6 | pclfinN 35707 |
| [PtakPulmannova] p. 74 | Lemma 3.3.10 | pclcmpatN 35708 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2758 rabid 3264 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2603 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2764 |
| [Quine] p. 19 | Definition 2.9 | conventions 27599 df-v 3353 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2881 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2893 abid2f 2940 |
| [Quine] p. 40 | Theorem 6.1 | sb5 2273 |
| [Quine] p. 40 | Theorem 6.2 | sb56 2271 sb6 2272 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2767 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2771 eqid1 27665 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2778 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3588 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3589 dfsbcq2 3590 |
| [Quine] p. 43 | Theorem 6.8 | vex 3354 |
| [Quine] p. 43 | Theorem 6.9 | isset 3359 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 3439 spcgv 3444 spcimgf 3437 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3600 spsbcd 3601 |
| [Quine] p. 44 | Theorem 6.12 | elex 3364 |
| [Quine] p. 44 | Theorem 6.13 | elab 3501 elabg 3502 elabgf 3499 |
| [Quine] p. 44 | Theorem 6.14 | noel 4067 |
| [Quine] p. 48 | Theorem 7.2 | snprc 4390 |
| [Quine] p. 48 | Definition 7.1 | df-pr 4320 df-sn 4318 |
| [Quine] p. 49 | Theorem 7.4 | snss 4452 snssg 4451 |
| [Quine] p. 49 | Theorem 7.5 | prss 4487 prssg 4486 |
| [Quine] p. 49 | Theorem 7.6 | prid1 4434 prid1g 4432 prid2 4435 prid2g 4433 snid 4348 snidg 4346 |
| [Quine] p. 51 | Theorem 7.12 | snex 5037 |
| [Quine] p. 51 | Theorem 7.13 | prex 5038 |
| [Quine] p. 53 | Theorem 8.2 | unisn 4590 unisnALT 39682 unisng 4591 |
| [Quine] p. 53 | Theorem 8.3 | uniun 4594 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 4604 |
| [Quine] p. 54 | Theorem 8.7 | uni0 4602 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 6003 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5994 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 6004 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 6008 |
| [Quine] p. 58 | Theorem 8.23 | iotaex 6010 |
| [Quine] p. 58 | Definition 9.1 | df-op 4324 |
| [Quine] p. 61 | Theorem 9.5 | opabid 5116 opelopab 5131 opelopaba 5125 opelopabaf 5133 opelopabf 5134 opelopabg 5127 opelopabga 5122 opelopabgf 5129 oprabid 6826 |
| [Quine] p. 64 | Definition 9.11 | df-xp 5256 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 5258 |
| [Quine] p. 64 | Definition 9.15 | df-id 5158 |
| [Quine] p. 65 | Theorem 10.3 | fun0 6093 |
| [Quine] p. 65 | Theorem 10.4 | funi 6062 |
| [Quine] p. 65 | Theorem 10.5 | funsn 6081 funsng 6079 |
| [Quine] p. 65 | Definition 10.1 | df-fun 6032 |
| [Quine] p. 65 | Definition 10.2 | args 5633 dffv4 6330 |
| [Quine] p. 68 | Definition 10.11 | conventions 27599 df-fv 6038 fv2 6328 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 13263 nn0opth2i 13262 nn0opthi 13261 omopthi 7895 |
| [Quine] p. 177 | Definition 25.2 | df-rdg 7663 |
| [Quine] p. 232 | Equation i | carddom 9582 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 6115 funimaexg 6114 |
| [Quine] p. 331 | Axiom system NF | ru 3586 |
| [ReedSimon] p. 36 | Definition (iii) | ax-his3 28281 |
| [ReedSimon] p. 63 | Exercise 4(a) | df-dip 27896 polid 28356 polid2i 28354 polidi 28355 |
| [ReedSimon] p. 63 | Exercise 4(b) | df-ph 28008 |
| [ReedSimon] p. 195 | Remark | lnophm 29218 lnophmi 29217 |
| [Retherford] p. 49 | Exercise 1(i) | leopadd 29331 |
| [Retherford] p. 49 | Exercise 1(ii) | leopmul 29333 leopmuli 29332 |
| [Retherford] p. 49 | Exercise 1(iv) | leoptr 29336 |
| [Retherford] p. 49 | Definition VI.1 | df-leop 29051 leoppos 29325 |
| [Retherford] p. 49 | Exercise 1(iii) | leoptri 29335 |
| [Retherford] p. 49 | Definition of operator ordering | leop3 29324 |
| [Roman] p. 4 | Definition | df-dmat 20514 df-dmatalt 42710 |
| [Roman] p. 18 | Part Preliminaries | df-rng0 42398 |
| [Roman] p. 19 | Part Preliminaries | df-ring 18757 |
| [Roman] p. 46 | Theorem 1.6 | isldepslvec2 42797 |
| [Roman] p. 112 | Note | isldepslvec2 42797 ldepsnlinc 42820 zlmodzxznm 42809 |
| [Roman] p. 112 | Example | zlmodzxzequa 42808 zlmodzxzequap 42811 zlmodzxzldep 42816 |
| [Roman] p. 170 | Theorem 7.8 | cayleyhamilton 20915 |
| [Rosenlicht] p. 80 | Theorem | heicant 33776 |
| [Rosser] p. 281 | Definition | df-op 4324 |
| [RosserSchoenfeld] p. 71 | Theorem 12. | ax-ros335 31063 |
| [RosserSchoenfeld] p. 71 | Theorem 13. | ax-ros336 31064 |
| [Rotman] p. 28 | Remark | pgrpgt2nabl 42670 pmtr3ncom 18102 |
| [Rotman] p. 31 | Theorem 3.4 | symggen2 18098 |
| [Rotman] p. 42 | Theorem 3.15 | cayley 18041 cayleyth 18042 |
| [Rudin] p. 164 | Equation 27 | efcan 15032 |
| [Rudin] p. 164 | Equation 30 | efzval 15038 |
| [Rudin] p. 167 | Equation 48 | absefi 15132 |
| [Sanford] p. 39 | Remark | ax-mp 5 mto 188 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1844 |
| [Sanford] p. 39 | Rule 4 | mptxor 1842 |
| [Sanford] p. 40 | Rule 1 | mptnan 1841 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5651 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5654 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5650 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5648 |
| [Schechter] p. 78 | Definition of Moore collection of sets | df-mre 16454 |
| [Schechter] p. 79 | Definition of Moore closure | df-mrc 16455 |
| [Schechter] p. 82 | Section 4.5 | df-mrc 16455 |
| [Schechter] p. 84 | Definition (A) of an algebraic closure system | df-acs 16457 |
| [Schechter] p. 139 | Definition AC3 | dfac9 9164 |
| [Schechter] p. 141 | Definition (MC) | dfac11 38156 |
| [Schechter] p. 149 | Axiom DC1 | ax-dc 9474 axdc3 9482 |
| [Schechter] p. 187 | Definition of ring with unit | isring 18759 isrngo 34026 |
| [Schechter] p. 276 | Remark 11.6.e | span0 28741 |
| [Schechter] p. 276 | Definition of span | df-span 28508 spanval 28532 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 21018 |
| [Schwabhauser] p. 10 | Axiom A1 | axcgrrflx 26015 axtgcgrrflx 25582 |
| [Schwabhauser] p. 10 | Axiom A2 | axcgrtr 26016 |
| [Schwabhauser] p. 10 | Axiom A3 | axcgrid 26017 axtgcgrid 25583 |
| [Schwabhauser] p. 10 | Axioms A1 to A3 | df-trkgc 25568 |
| [Schwabhauser] p. 11 | Axiom A4 | axsegcon 26028 axtgsegcon 25584 df-trkgcb 25570 |
| [Schwabhauser] p. 11 | Axiom A5 | ax5seg 26039 axtg5seg 25585 df-trkgcb 25570 |
| [Schwabhauser] p. 11 | Axiom A6 | axbtwnid 26040 axtgbtwnid 25586 df-trkgb 25569 |
| [Schwabhauser] p. 12 | Axiom A7 | axpasch 26042 axtgpasch 25587 df-trkgb 25569 |
| [Schwabhauser] p. 12 | Axiom A8 | axlowdim2 26061 df-trkg2d 31083 |
| [Schwabhauser] p. 13 | Axiom A8 | axtglowdim2 25590 |
| [Schwabhauser] p. 13 | Axiom A9 | axtgupdim2 25591 df-trkg2d 31083 |
| [Schwabhauser] p. 13 | Axiom A10 | axeuclid 26064 axtgeucl 25592 df-trkge 25571 |
| [Schwabhauser] p. 13 | Axiom A11 | axcont 26077 axtgcont 25589 axtgcont1 25588 df-trkgb 25569 |
| [Schwabhauser] p. 27 | Theorem 2.1 | cgrrflx 32431 |
| [Schwabhauser] p. 27 | Theorem 2.2 | cgrcomim 32433 |
| [Schwabhauser] p. 27 | Theorem 2.3 | cgrtr 32436 |
| [Schwabhauser] p. 27 | Theorem 2.4 | cgrcoml 32440 |
| [Schwabhauser] p. 27 | Theorem 2.5 | cgrcomr 32441 tgcgrcomimp 25593 tgcgrcoml 25595 tgcgrcomr 25594 |
| [Schwabhauser] p. 28 | Theorem 2.8 | cgrtriv 32446 tgcgrtriv 25600 |
| [Schwabhauser] p. 28 | Theorem 2.10 | 5segofs 32450 tg5segofs 31091 |
| [Schwabhauser] p. 28 | Definition 2.10 | df-afs 31088 df-ofs 32427 |
| [Schwabhauser] p. 29 | Theorem 2.11 | cgrextend 32452 tgcgrextend 25601 |
| [Schwabhauser] p. 29 | Theorem 2.12 | segconeq 32454 tgsegconeq 25602 |
| [Schwabhauser] p. 30 | Theorem 3.1 | btwnouttr2 32466 btwntriv2 32456 tgbtwntriv2 25603 |
| [Schwabhauser] p. 30 | Theorem 3.2 | btwncomim 32457 tgbtwncom 25604 |
| [Schwabhauser] p. 30 | Theorem 3.3 | btwntriv1 32460 tgbtwntriv1 25607 |
| [Schwabhauser] p. 30 | Theorem 3.4 | btwnswapid 32461 tgbtwnswapid 25608 |
| [Schwabhauser] p. 30 | Theorem 3.5 | btwnexch2 32467 btwnintr 32463 tgbtwnexch2 25612 tgbtwnintr 25609 |
| [Schwabhauser] p. 30 | Theorem 3.6 | btwnexch 32469 btwnexch3 32464 tgbtwnexch 25614 tgbtwnexch3 25610 |
| [Schwabhauser] p. 30 | Theorem 3.7 | btwnouttr 32468 tgbtwnouttr 25613 tgbtwnouttr2 25611 |
| [Schwabhauser] p. 32 | Theorem 3.13 | axlowdim1 26060 |
| [Schwabhauser] p. 32 | Theorem 3.14 | btwndiff 32471 tgbtwndiff 25622 |
| [Schwabhauser] p. 33 | Theorem 3.17 | tgtrisegint 25615 trisegint 32472 |
| [Schwabhauser] p. 34 | Theorem 4.2 | ifscgr 32488 tgifscgr 25624 |
| [Schwabhauser] p. 34 | Theorem 4.11 | colcom 25674 colrot1 25675 colrot2 25676 lncom 25738 lnrot1 25739 lnrot2 25740 |
| [Schwabhauser] p. 34 | Definition 4.1 | df-ifs 32484 |
| [Schwabhauser] p. 35 | Theorem 4.3 | cgrsub 32489 tgcgrsub 25625 |
| [Schwabhauser] p. 35 | Theorem 4.5 | cgrxfr 32499 tgcgrxfr 25634 |
| [Schwabhauser] p. 35 | Statement 4.4 | ercgrg 25633 |
| [Schwabhauser] p. 35 | Definition 4.4 | df-cgr3 32485 df-cgrg 25627 |
| [Schwabhauser] p. 36 | Theorem 4.6 | btwnxfr 32500 tgbtwnxfr 25646 |
| [Schwabhauser] p. 36 | Theorem 4.11 | colinearperm1 32506 colinearperm2 32508 colinearperm3 32507 colinearperm4 32509 colinearperm5 32510 |
| [Schwabhauser] p. 36 | Definition 4.8 | df-ismt 25649 |
| [Schwabhauser] p. 36 | Definition 4.10 | df-colinear 32483 tgellng 25669 tglng 25662 |
| [Schwabhauser] p. 37 | Theorem 4.12 | colineartriv1 32511 |
| [Schwabhauser] p. 37 | Theorem 4.13 | colinearxfr 32519 lnxfr 25682 |
| [Schwabhauser] p. 37 | Theorem 4.14 | lineext 32520 lnext 25683 |
| [Schwabhauser] p. 37 | Theorem 4.16 | fscgr 32524 tgfscgr 25684 |
| [Schwabhauser] p. 37 | Theorem 4.17 | linecgr 32525 lncgr 25685 |
| [Schwabhauser] p. 37 | Definition 4.15 | df-fs 32486 |
| [Schwabhauser] p. 38 | Theorem 4.18 | lineid 32527 lnid 25686 |
| [Schwabhauser] p. 38 | Theorem 4.19 | idinside 32528 tgidinside 25687 |
| [Schwabhauser] p. 39 | Theorem 5.1 | btwnconn1 32545 tgbtwnconn1 25691 |
| [Schwabhauser] p. 41 | Theorem 5.2 | btwnconn2 32546 tgbtwnconn2 25692 |
| [Schwabhauser] p. 41 | Theorem 5.3 | btwnconn3 32547 tgbtwnconn3 25693 |
| [Schwabhauser] p. 41 | Theorem 5.5 | brsegle2 32553 |
| [Schwabhauser] p. 41 | Definition 5.4 | df-segle 32551 legov 25701 |
| [Schwabhauser] p. 41 | Definition 5.5 | legov2 25702 |
| [Schwabhauser] p. 42 | Remark 5.13 | legso 25715 |
| [Schwabhauser] p. 42 | Theorem 5.6 | seglecgr12im 32554 |
| [Schwabhauser] p. 42 | Theorem 5.7 | seglerflx 32556 |
| [Schwabhauser] p. 42 | Theorem 5.8 | segletr 32558 |
| [Schwabhauser] p. 42 | Theorem 5.9 | segleantisym 32559 |
| [Schwabhauser] p. 42 | Theorem 5.10 | seglelin 32560 |
| [Schwabhauser] p. 42 | Theorem 5.11 | seglemin 32557 |
| [Schwabhauser] p. 42 | Theorem 5.12 | colinbtwnle 32562 |
| [Schwabhauser] p. 42 | Proposition 5.7 | legid 25703 |
| [Schwabhauser] p. 42 | Proposition 5.8 | legtrd 25705 |
| [Schwabhauser] p. 42 | Proposition 5.9 | legtri3 25706 |
| [Schwabhauser] p. 42 | Proposition 5.10 | legtrid 25707 |
| [Schwabhauser] p. 42 | Proposition 5.11 | leg0 25708 |
| [Schwabhauser] p. 43 | Theorem 6.2 | btwnoutside 32569 |
| [Schwabhauser] p. 43 | Theorem 6.3 | broutsideof3 32570 |
| [Schwabhauser] p. 43 | Theorem 6.4 | broutsideof 32565 df-outsideof 32564 |
| [Schwabhauser] p. 43 | Definition 6.1 | broutsideof2 32566 ishlg 25718 |
| [Schwabhauser] p. 44 | Theorem 6.4 | hlln 25723 |
| [Schwabhauser] p. 44 | Theorem 6.5 | hlid 25725 outsideofrflx 32571 |
| [Schwabhauser] p. 44 | Theorem 6.6 | hlcomb 25719 hlcomd 25720 outsideofcom 32572 |
| [Schwabhauser] p. 44 | Theorem 6.7 | hltr 25726 outsideoftr 32573 |
| [Schwabhauser] p. 44 | Theorem 6.11 | hlcgreu 25734 outsideofeu 32575 |
| [Schwabhauser] p. 44 | Definition 6.8 | df-ray 32582 |
| [Schwabhauser] p. 45 | Part 2 | df-lines2 32583 |
| [Schwabhauser] p. 45 | Theorem 6.13 | outsidele 32576 |
| [Schwabhauser] p. 45 | Theorem 6.15 | lineunray 32591 |
| [Schwabhauser] p. 45 | Theorem 6.16 | lineelsb2 32592 tglineelsb2 25748 |
| [Schwabhauser] p. 45 | Theorem 6.17 | linecom 32594 linerflx1 32593 linerflx2 32595 tglinecom 25751 tglinerflx1 25749 tglinerflx2 25750 |
| [Schwabhauser] p. 45 | Theorem 6.18 | linethru 32597 tglinethru 25752 |
| [Schwabhauser] p. 45 | Definition 6.14 | df-line2 32581 tglng 25662 |
| [Schwabhauser] p. 45 | Proposition 6.13 | legbtwn 25710 |
| [Schwabhauser] p. 46 | Theorem 6.19 | linethrueu 32600 tglinethrueu 25755 |
| [Schwabhauser] p. 46 | Theorem 6.21 | lineintmo 32601 tglineineq 25759 tglineinteq 25761 tglineintmo 25758 |
| [Schwabhauser] p. 46 | Theorem 6.23 | colline 25765 |
| [Schwabhauser] p. 46 | Theorem 6.24 | tglowdim2l 25766 |
| [Schwabhauser] p. 46 | Theorem 6.25 | tglowdim2ln 25767 |
| [Schwabhauser] p. 49 | Theorem 7.3 | mirinv 25782 |
| [Schwabhauser] p. 49 | Theorem 7.7 | mirmir 25778 |
| [Schwabhauser] p. 49 | Theorem 7.8 | mirreu3 25770 |
| [Schwabhauser] p. 49 | Definition 7.5 | df-mir 25769 ismir 25775 mirbtwn 25774 mircgr 25773 mirfv 25772 mirval 25771 |
| [Schwabhauser] p. 50 | Theorem 7.8 | mirreu 25780 |
| [Schwabhauser] p. 50 | Theorem 7.9 | mireq 25781 |
| [Schwabhauser] p. 50 | Theorem 7.10 | mirinv 25782 |
| [Schwabhauser] p. 50 | Theorem 7.11 | mirf1o 25785 |
| [Schwabhauser] p. 50 | Theorem 7.13 | miriso 25786 |
| [Schwabhauser] p. 51 | Theorem 7.14 | mirmot 25791 |
| [Schwabhauser] p. 51 | Theorem 7.15 | mirbtwnb 25788 mirbtwni 25787 |
| [Schwabhauser] p. 51 | Theorem 7.16 | mircgrs 25789 |
| [Schwabhauser] p. 51 | Theorem 7.17 | miduniq 25801 |
| [Schwabhauser] p. 52 | Lemma 7.21 | symquadlem 25805 |
| [Schwabhauser] p. 52 | Theorem 7.18 | miduniq1 25802 |
| [Schwabhauser] p. 52 | Theorem 7.19 | miduniq2 25803 |
| [Schwabhauser] p. 52 | Theorem 7.20 | colmid 25804 |
| [Schwabhauser] p. 53 | Lemma 7.22 | krippen 25807 |
| [Schwabhauser] p. 55 | Lemma 7.25 | midexlem 25808 |
| [Schwabhauser] p. 57 | Theorem 8.2 | ragcom 25814 |
| [Schwabhauser] p. 57 | Definition 8.1 | df-rag 25810 israg 25813 |
| [Schwabhauser] p. 58 | Theorem 8.3 | ragcol 25815 |
| [Schwabhauser] p. 58 | Theorem 8.4 | ragmir 25816 |
| [Schwabhauser] p. 58 | Theorem 8.5 | ragtrivb 25818 |
| [Schwabhauser] p. 58 | Theorem 8.6 | ragflat2 25819 |
| [Schwabhauser] p. 58 | Theorem 8.7 | ragflat 25820 |
| [Schwabhauser] p. 58 | Theorem 8.8 | ragtriva 25821 |
| [Schwabhauser] p. 58 | Theorem 8.9 | ragflat3 25822 ragncol 25825 |
| [Schwabhauser] p. 58 | Theorem 8.10 | ragcgr 25823 |
| [Schwabhauser] p. 59 | Theorem 8.12 | perpcom 25829 |
| [Schwabhauser] p. 59 | Theorem 8.13 | ragperp 25833 |
| [Schwabhauser] p. 59 | Theorem 8.14 | perpneq 25830 |
| [Schwabhauser] p. 59 | Definition 8.11 | df-perpg 25812 isperp 25828 |
| [Schwabhauser] p. 59 | Definition 8.13 | isperp2 25831 |
| [Schwabhauser] p. 60 | Theorem 8.18 | foot 25835 |
| [Schwabhauser] p. 62 | Lemma 8.20 | colperpexlem1 25843 colperpexlem2 25844 |
| [Schwabhauser] p. 63 | Theorem 8.21 | colperpex 25846 colperpexlem3 25845 |
| [Schwabhauser] p. 64 | Theorem 8.22 | mideu 25851 midex 25850 |
| [Schwabhauser] p. 66 | Lemma 8.24 | opphllem 25848 |
| [Schwabhauser] p. 67 | Theorem 9.2 | oppcom 25857 |
| [Schwabhauser] p. 67 | Definition 9.1 | islnopp 25852 |
| [Schwabhauser] p. 68 | Lemma 9.3 | opphllem2 25861 |
| [Schwabhauser] p. 68 | Lemma 9.4 | opphllem5 25864 opphllem6 25865 |
| [Schwabhauser] p. 69 | Theorem 9.5 | opphl 25867 |
| [Schwabhauser] p. 69 | Theorem 9.6 | axtgpasch 25587 |
| [Schwabhauser] p. 70 | Theorem 9.6 | outpasch 25868 |
| [Schwabhauser] p. 71 | Theorem 9.8 | lnopp2hpgb 25876 |
| [Schwabhauser] p. 71 | Definition 9.7 | df-hpg 25871 hpgbr 25873 |
| [Schwabhauser] p. 72 | Lemma 9.10 | hpgerlem 25878 |
| [Schwabhauser] p. 72 | Theorem 9.9 | lnoppnhpg 25877 |
| [Schwabhauser] p. 72 | Theorem 9.11 | hpgid 25879 |
| [Schwabhauser] p. 72 | Theorem 9.12 | hpgcom 25880 |
| [Schwabhauser] p. 72 | Theorem 9.13 | hpgtr 25881 |
| [Schwabhauser] p. 73 | Theorem 9.18 | colopp 25882 |
| [Schwabhauser] p. 73 | Theorem 9.19 | colhp 25883 |
| [Schwabhauser] p. 88 | Theorem 10.2 | lmieu 25897 |
| [Schwabhauser] p. 88 | Definition 10.1 | df-mid 25887 |
| [Schwabhauser] p. 89 | Theorem 10.4 | lmicom 25901 |
| [Schwabhauser] p. 89 | Theorem 10.5 | lmilmi 25902 |
| [Schwabhauser] p. 89 | Theorem 10.6 | lmireu 25903 |
| [Schwabhauser] p. 89 | Theorem 10.7 | lmieq 25904 |
| [Schwabhauser] p. 89 | Theorem 10.8 | lmiinv 25905 |
| [Schwabhauser] p. 89 | Theorem 10.9 | lmif1o 25908 |
| [Schwabhauser] p. 89 | Theorem 10.10 | lmiiso 25910 |
| [Schwabhauser] p. 89 | Definition 10.3 | df-lmi 25888 |
| [Schwabhauser] p. 90 | Theorem 10.11 | lmimot 25911 |
| [Schwabhauser] p. 91 | Theorem 10.12 | hypcgr 25914 |
| [Schwabhauser] p. 92 | Theorem 10.14 | lmiopp 25915 |
| [Schwabhauser] p. 92 | Theorem 10.15 | lnperpex 25916 |
| [Schwabhauser] p. 92 | Theorem 10.16 | trgcopy 25917 trgcopyeu 25919 |
| [Schwabhauser] p. 95 | Definition 11.2 | dfcgra2 25942 |
| [Schwabhauser] p. 95 | Definition 11.3 | iscgra 25922 |
| [Schwabhauser] p. 95 | Proposition 11.4 | cgracgr 25931 |
| [Schwabhauser] p. 95 | Proposition 11.10 | cgrahl1 25929 cgrahl2 25930 |
| [Schwabhauser] p. 96 | Theorem 11.6 | cgraid 25932 |
| [Schwabhauser] p. 96 | Theorem 11.9 | cgraswap 25933 |
| [Schwabhauser] p. 97 | Theorem 11.7 | cgracom 25935 |
| [Schwabhauser] p. 97 | Theorem 11.8 | cgratr 25936 |
| [Schwabhauser] p. 97 | Theorem 11.21 | cgrabtwn 25938 cgrahl 25939 |
| [Schwabhauser] p. 98 | Theorem 11.13 | sacgr 25943 |
| [Schwabhauser] p. 98 | Theorem 11.14 | oacgr 25944 |
| [Schwabhauser] p. 98 | Theorem 11.15 | acopy 25945 acopyeu 25946 |
| [Schwabhauser] p. 101 | Theorem 11.24 | inagswap 25951 |
| [Schwabhauser] p. 101 | Theorem 11.25 | inaghl 25952 |
| [Schwabhauser] p. 101 | Property for point ` ` to lie in the angle ` ` Defnition 11.23 | isinag 25950 |
| [Schwabhauser] p. 102 | Lemma 11.28 | cgrg3col4 25955 |
| [Schwabhauser] p. 102 | Definition 11.27 | df-leag 25953 isleag 25954 |
| [Schwabhauser] p. 107 | Theorem 11.49 | tgsas 25957 tgsas1 25956 tgsas2 25958 tgsas3 25959 |
| [Schwabhauser] p. 108 | Theorem 11.50 | tgasa 25961 tgasa1 25960 |
| [Schwabhauser] p. 109 | Theorem 11.51 | tgsss1 25962 tgsss2 25963 tgsss3 25964 |
| [Shapiro] p. 230 | Theorem 6.5.1 | dchrhash 25217 dchrsum 25215 dchrsum2 25214 sumdchr 25218 |
| [Shapiro] p. 232 | Theorem 6.5.2 | dchr2sum 25219 sum2dchr 25220 |
| [Shapiro], p. 199 | Lemma 6.1C.2 | ablfacrp 18673 ablfacrp2 18674 |
| [Shapiro], p. 328 | Equation 9.2.4 | vmasum 25162 |
| [Shapiro], p. 329 | Equation 9.2.7 | logfac2 25163 |
| [Shapiro], p. 329 | Equation 9.2.9 | logfacrlim 25170 |
| [Shapiro], p. 331 | Equation 9.2.13 | vmadivsum 25392 |
| [Shapiro], p. 331 | Equation 9.2.14 | rplogsumlem2 25395 |
| [Shapiro], p. 336 | Exercise 9.1.7 | vmalogdivsum 25449 vmalogdivsum2 25448 |
| [Shapiro], p. 375 | Theorem 9.4.1 | dirith 25439 dirith2 25438 |
| [Shapiro], p. 375 | Equation 9.4.3 | rplogsum 25437 rpvmasum 25436 rpvmasum2 25422 |
| [Shapiro], p. 376 | Equation 9.4.7 | rpvmasumlem 25397 |
| [Shapiro], p. 376 | Equation 9.4.8 | dchrvmasum 25435 |
| [Shapiro], p. 377 | Lemma 9.4.1 | dchrisum 25402 dchrisumlem1 25399 dchrisumlem2 25400 dchrisumlem3 25401 dchrisumlema 25398 |
| [Shapiro], p. 377 | Equation 9.4.11 | dchrvmasumlem1 25405 |
| [Shapiro], p. 379 | Equation 9.4.16 | dchrmusum 25434 dchrmusumlem 25432 dchrvmasumlem 25433 |
| [Shapiro], p. 380 | Lemma 9.4.2 | dchrmusum2 25404 |
| [Shapiro], p. 380 | Lemma 9.4.3 | dchrvmasum2lem 25406 |
| [Shapiro], p. 382 | Lemma 9.4.4 | dchrisum0 25430 dchrisum0re 25423 dchrisumn0 25431 |
| [Shapiro], p. 382 | Equation 9.4.27 | dchrisum0fmul 25416 |
| [Shapiro], p. 382 | Equation 9.4.29 | dchrisum0flb 25420 |
| [Shapiro], p. 383 | Equation 9.4.30 | dchrisum0fno1 25421 |
| [Shapiro], p. 403 | Equation 10.1.16 | pntrsumbnd 25476 pntrsumbnd2 25477 pntrsumo1 25475 |
| [Shapiro], p. 405 | Equation 10.2.1 | mudivsum 25440 |
| [Shapiro], p. 406 | Equation 10.2.6 | mulogsum 25442 |
| [Shapiro], p. 407 | Equation 10.2.7 | mulog2sumlem1 25444 |
| [Shapiro], p. 407 | Equation 10.2.8 | mulog2sum 25447 |
| [Shapiro], p. 418 | Equation 10.4.6 | logsqvma 25452 |
| [Shapiro], p. 418 | Equation 10.4.8 | logsqvma2 25453 |
| [Shapiro], p. 419 | Equation 10.4.10 | selberg 25458 |
| [Shapiro], p. 420 | Equation 10.4.12 | selberg2lem 25460 |
| [Shapiro], p. 420 | Equation 10.4.14 | selberg2 25461 |
| [Shapiro], p. 422 | Equation 10.6.7 | selberg3 25469 |
| [Shapiro], p. 422 | Equation 10.4.20 | selberg4lem1 25470 |
| [Shapiro], p. 422 | Equation 10.4.21 | selberg3lem1 25467 selberg3lem2 25468 |
| [Shapiro], p. 422 | Equation 10.4.23 | selberg4 25471 |
| [Shapiro], p. 427 | Theorem 10.5.2 | chpdifbnd 25465 |
| [Shapiro], p. 428 | Equation 10.6.2 | selbergr 25478 |
| [Shapiro], p. 429 | Equation 10.6.8 | selberg3r 25479 |
| [Shapiro], p. 430 | Equation 10.6.11 | selberg4r 25480 |
| [Shapiro], p. 431 | Equation 10.6.15 | pntrlog2bnd 25494 |
| [Shapiro], p. 434 | Equation 10.6.27 | pntlema 25506 pntlemb 25507 pntlemc 25505 pntlemd 25504 pntlemg 25508 |
| [Shapiro], p. 435 | Equation 10.6.29 | pntlema 25506 |
| [Shapiro], p. 436 | Lemma 10.6.1 | pntpbnd 25498 |
| [Shapiro], p. 436 | Lemma 10.6.2 | pntibnd 25503 |
| [Shapiro], p. 436 | Equation 10.6.34 | pntlema 25506 |
| [Shapiro], p. 436 | Equation 10.6.35 | pntlem3 25519 pntleml 25521 |
| [Stoll] p. 13 | Definition corresponds to | dfsymdif3 4041 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 4122 dif0 4098 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdir 4199 |
| [Stoll] p. 17 | Theorem 5.1(5) | unvdif 4185 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 4034 |
| [Stoll] p. 19 | Theorem 5.2(13') | indm 4035 |
| [Stoll] p. 20 | Remark | invdif 4017 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 4326 |
| [Stoll] p. 43 | Definition | uniiun 4708 |
| [Stoll] p. 44 | Definition | intiin 4709 |
| [Stoll] p. 45 | Definition | df-iin 4658 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4657 |
| [Stoll] p. 176 | Theorem 3.4(27) | iman 388 |
| [Stoll] p. 262 | Example 4.1 | dfsymdif3 4041 |
| [Strang] p. 242 | Section 6.3 | expgrowth 39058 |
| [Suppes] p. 22 | Theorem 2 | eq0 4077 eq0f 4074 |
| [Suppes] p. 22 | Theorem 4 | eqss 3767 eqssd 3769 eqssi 3768 |
| [Suppes] p. 23 | Theorem 5 | ss0 4119 ss0b 4118 |
| [Suppes] p. 23 | Theorem 6 | sstr 3760 sstrALT2 39590 |
| [Suppes] p. 23 | Theorem 7 | pssirr 3857 |
| [Suppes] p. 23 | Theorem 8 | pssn2lp 3858 |
| [Suppes] p. 23 | Theorem 9 | psstr 3861 |
| [Suppes] p. 23 | Theorem 10 | pssss 3852 |
| [Suppes] p. 25 | Theorem 12 | elin 3947 elun 3904 |
| [Suppes] p. 26 | Theorem 15 | inidm 3971 |
| [Suppes] p. 26 | Theorem 16 | in0 4113 |
| [Suppes] p. 27 | Theorem 23 | unidm 3907 |
| [Suppes] p. 27 | Theorem 24 | un0 4112 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3927 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3934 |
| [Suppes] p. 27 | Theorem 27 | unss 3938 |
| [Suppes] p. 27 | Theorem 28 | indir 4024 |
| [Suppes] p. 27 | Theorem 29 | undir 4025 |
| [Suppes] p. 28 | Theorem 32 | difid 4096 |
| [Suppes] p. 29 | Theorem 33 | difin 4010 |
| [Suppes] p. 29 | Theorem 34 | indif 4018 |
| [Suppes] p. 29 | Theorem 35 | undif1 4186 |
| [Suppes] p. 29 | Theorem 36 | difun2 4191 |
| [Suppes] p. 29 | Theorem 37 | difin0 4184 |
| [Suppes] p. 29 | Theorem 38 | disjdif 4183 |
| [Suppes] p. 29 | Theorem 39 | difundi 4028 |
| [Suppes] p. 29 | Theorem 40 | difindi 4030 |
| [Suppes] p. 30 | Theorem 41 | nalset 4930 |
| [Suppes] p. 39 | Theorem 61 | uniss 4596 |
| [Suppes] p. 39 | Theorem 65 | uniop 5109 |
| [Suppes] p. 41 | Theorem 70 | intsn 4648 |
| [Suppes] p. 42 | Theorem 71 | intpr 4645 intprg 4646 |
| [Suppes] p. 42 | Theorem 73 | op1stb 5068 |
| [Suppes] p. 42 | Theorem 78 | intun 4644 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4689 dfiun2g 4687 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4690 |
| [Suppes] p. 47 | Theorem 86 | elpw 4304 elpw2 4960 elpw2g 4959 elpwg 4306 elpwgdedVD 39673 |
| [Suppes] p. 47 | Theorem 87 | pwid 4314 |
| [Suppes] p. 47 | Theorem 89 | pw0 4479 |
| [Suppes] p. 48 | Theorem 90 | pwpw0 4480 |
| [Suppes] p. 52 | Theorem 101 | xpss12 5265 |
| [Suppes] p. 52 | Theorem 102 | xpindi 5393 xpindir 5394 |
| [Suppes] p. 52 | Theorem 103 | xpundi 5310 xpundir 5311 |
| [Suppes] p. 54 | Theorem 105 | elirrv 8661 |
| [Suppes] p. 58 | Theorem 2 | relss 5345 |
| [Suppes] p. 59 | Theorem 4 | eldm 5458 eldm2 5459 eldm2g 5457 eldmg 5456 |
| [Suppes] p. 59 | Definition 3 | df-dm 5260 |
| [Suppes] p. 60 | Theorem 6 | dmin 5469 |
| [Suppes] p. 60 | Theorem 8 | rnun 5681 |
| [Suppes] p. 60 | Theorem 9 | rnin 5682 |
| [Suppes] p. 60 | Definition 4 | dfrn2 5448 |
| [Suppes] p. 61 | Theorem 11 | brcnv 5442 brcnvg 5440 |
| [Suppes] p. 62 | Equation 5 | elcnv 5436 elcnv2 5437 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5643 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5680 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5678 |
| [Suppes] p. 63 | Theorem 20 | co02 5792 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5522 |
| [Suppes] p. 63 | Definition 7 | df-co 5259 |
| [Suppes] p. 64 | Theorem 26 | cnvco 5445 |
| [Suppes] p. 64 | Theorem 27 | coass 5797 |
| [Suppes] p. 65 | Theorem 31 | resundi 5550 |
| [Suppes] p. 65 | Theorem 34 | elima 5611 elima2 5612 elima3 5613 elimag 5610 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5685 |
| [Suppes] p. 66 | Theorem 40 | dminss 5687 |
| [Suppes] p. 66 | Theorem 41 | imainss 5688 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5691 |
| [Suppes] p. 81 | Definition 34 | dfec2 7903 |
| [Suppes] p. 82 | Theorem 72 | elec 7942 elecALTV 34371 elecg 7941 |
| [Suppes] p. 82 | Theorem 73 | erth 7947 erth2 7948 |
| [Suppes] p. 83 | Theorem 74 | erdisj 7950 |
| [Suppes] p. 89 | Theorem 96 | map0b 8053 |
| [Suppes] p. 89 | Theorem 97 | map0 8056 map0g 8054 |
| [Suppes] p. 89 | Theorem 98 | mapsn 8057 mapsnd 8055 |
| [Suppes] p. 89 | Theorem 99 | mapss 8058 |
| [Suppes] p. 91 | Definition 12(ii) | alephsuc 9095 |
| [Suppes] p. 91 | Definition 12(iii) | alephlim 9094 |
| [Suppes] p. 92 | Theorem 1 | enref 8146 enrefg 8145 |
| [Suppes] p. 92 | Theorem 2 | ensym 8162 ensymb 8161 ensymi 8163 |
| [Suppes] p. 92 | Theorem 3 | entr 8165 |
| [Suppes] p. 92 | Theorem 4 | unen 8200 |
| [Suppes] p. 94 | Theorem 15 | endom 8140 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 8159 |
| [Suppes] p. 94 | Theorem 17 | domtr 8166 |
| [Suppes] p. 95 | Theorem 18 | sbth 8240 |
| [Suppes] p. 97 | Theorem 23 | canth2 8273 canth2g 8274 |
| [Suppes] p. 97 | Definition 3 | brsdom2 8244 df-sdom 8116 dfsdom2 8243 |
| [Suppes] p. 97 | Theorem 21(i) | sdomirr 8257 |
| [Suppes] p. 97 | Theorem 22(i) | domnsym 8246 |
| [Suppes] p. 97 | Theorem 21(ii) | sdomnsym 8245 |
| [Suppes] p. 97 | Theorem 22(ii) | domsdomtr 8255 |
| [Suppes] p. 97 | Theorem 22(iv) | brdom2 8143 |
| [Suppes] p. 97 | Theorem 21(iii) | sdomtr 8258 |
| [Suppes] p. 97 | Theorem 22(iii) | sdomdomtr 8253 |
| [Suppes] p. 98 | Exercise 4 | fundmen 8187 fundmeng 8188 |
| [Suppes] p. 98 | Exercise 6 | xpdom3 8218 |
| [Suppes] p. 98 | Exercise 11 | sdomentr 8254 |
| [Suppes] p. 104 | Theorem 37 | fofi 8412 |
| [Suppes] p. 104 | Theorem 38 | pwfi 8421 |
| [Suppes] p. 105 | Theorem 40 | pwfi 8421 |
| [Suppes] p. 111 | Axiom for cardinal numbers | carden 9579 |
| [Suppes] p. 130 | Definition 3 | df-tr 4888 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 7137 |
| [Suppes] p. 134 | Definition 6 | df-suc 5871 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 7247 finds 7243 finds1 7246 finds2 7245 |
| [Suppes] p. 151 | Theorem 42 | isfinite 8717 isfinite2 8378 isfiniteg 8380 unbnn 8376 |
| [Suppes] p. 162 | Definition 5 | df-ltnq 9946 df-ltpq 9938 |
| [Suppes] p. 197 | Theorem Schema 4 | tfindes 7213 tfinds 7210 tfinds2 7214 |
| [Suppes] p. 209 | Theorem 18 | oaord1 7789 |
| [Suppes] p. 209 | Theorem 21 | oaword2 7791 |
| [Suppes] p. 211 | Theorem 25 | oaass 7799 |
| [Suppes] p. 225 | Definition 8 | iscard2 9006 |
| [Suppes] p. 227 | Theorem 56 | ondomon 9591 |
| [Suppes] p. 228 | Theorem 59 | harcard 9008 |
| [Suppes] p. 228 | Definition 12(i) | aleph0 9093 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 5917 |
| [Suppes] p. 228 | Theorem Schema 62 | onminesb 7149 onminsb 7150 |
| [Suppes] p. 229 | Theorem 64 | alephval2 9600 |
| [Suppes] p. 229 | Theorem 65 | alephcard 9097 |
| [Suppes] p. 229 | Theorem 66 | alephord2i 9104 |
| [Suppes] p. 229 | Theorem 67 | alephnbtwn 9098 |
| [Suppes] p. 229 | Definition 12 | df-aleph 8970 |
| [Suppes] p. 242 | Theorem 6 | weth 9523 |
| [Suppes] p. 242 | Theorem 8 | entric 9585 |
| [Suppes] p. 242 | Theorem 9 | carden 9579 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2751 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2764 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2767 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2766 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2790 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6800 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3586 |
| [TakeutiZaring] p. 15 | Axiom 2 | zfpair 5033 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 4339 elpr2 4340 elprg 4337 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 4332 elsn2 4351 elsn2g 4350 elsng 4331 velsn 4333 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 5064 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 4327 sneqr 4505 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 4335 dfsn2 4330 dfsn2ALT 4336 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 7104 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 5073 |
| [TakeutiZaring] p. 16 | Exercise 7 | opex 5061 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 5045 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 7107 unexg 7110 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 4369 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 4576 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3730 df-un 3728 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 4588 uniprg 4589 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4980 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 4368 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 5936 elsucg 5934 sstr2 3759 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3908 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3956 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3921 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3972 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 4022 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 4023 |
| [TakeutiZaring] p. 17 | Definition 5.9 | df-pss 3739 dfss2 3740 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 4300 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3935 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3737 sseqin2 3968 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3773 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3981 inss2 3982 |
| [TakeutiZaring] p. 18 | Exercise 13 | nss 3812 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 4583 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 5046 sspwimp 39674 sspwimpALT 39681 sspwimpALT2 39684 sspwimpcf 39676 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 5054 |
| [TakeutiZaring] p. 19 | Axiom 5 | ax-rep 4905 |
| [TakeutiZaring] p. 20 | Definition | df-rab 3070 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4925 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3726 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 4065 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 4096 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0 4079 n0f 4076 neq0 4078 neq0f 4075 |
| [TakeutiZaring] p. 21 | Axiom 6 | zfreg 8660 |
| [TakeutiZaring] p. 21 | Axiom 6' | zfregs 8776 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 8778 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 3353 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4932 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 4117 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4937 ssexg 4939 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4934 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 8667 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 8662 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0 4090 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3887 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3 4037 undif3VD 39638 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3888 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3895 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 3066 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 3067 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 7113 xpexg 7111 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 5257 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 6099 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 6251 fun11 6102 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 6042 svrelfun 6100 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 5447 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 5449 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 5262 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 5263 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 5259 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5729 dfrel2 5723 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 5266 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 5373 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 5379 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 5392 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5566 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5541 opelresALTV 34372 opelresg 5539 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5559 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5562 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5567 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 6071 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5776 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 6070 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 6252 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2658 |
| [TakeutiZaring] p. 26 | Definition 6.11 | conventions 27599 df-fv 6038 fv3 6349 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 7264 cnvexg 7263 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 7250 dmexg 7248 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 7251 rnexg 7249 |
| [TakeutiZaring] p. 26 | Corollary 6.9(1) | xpexb 39181 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnv 7259 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | fvex 6344 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1-afv 41769 tz6.12-1 6353 tz6.12-afv 41768 tz6.12 6354 tz6.12c 6356 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 6324 tz6.12i 6357 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 6033 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 6034 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 6036 wfo 6028 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 6035 wf1 6027 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 6037 wf1o 6029 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 6456 eqfnfv2 6457 eqfnfv2f 6460 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 6418 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 6628 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 6626 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 6115 funimaexg 6114 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4788 |
| [TakeutiZaring] p. 29 | Definition 6.19(1) | df-so 5172 |
| [TakeutiZaring] p. 30 | Definition 6.21 | dffr2 5215 dffr3 5638 eliniseg 5634 iniseg 5636 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 5163 |
| [TakeutiZaring] p. 30 | Proposition 6.23 | fr2nr 5228 fr3nr 7130 frirr 5227 |
| [TakeutiZaring] p. 30 | Definition 6.24(1) | df-fr 5209 |
| [TakeutiZaring] p. 30 | Definition 6.24(2) | dfwe2 7132 |
| [TakeutiZaring] p. 31 | Exercise 1 | frss 5217 |
| [TakeutiZaring] p. 31 | Exercise 4 | wess 5237 |
| [TakeutiZaring] p. 31 | Proposition 6.26 | tz6.26 5853 tz6.26i 5854 wefrc 5244 wereu2 5247 |
| [TakeutiZaring] p. 32 | Theorem 6.27 | wfi 5855 wfii 5856 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 6039 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 6725 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 6726 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 6732 |
| [TakeutiZaring] p. 33 | Proposition 6.31(1) | isomin 6733 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 6734 |
| [TakeutiZaring] p. 33 | Proposition 6.32(1) | isofr 6738 |
| [TakeutiZaring] p. 33 | Proposition 6.32(3) | isowe 6745 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 6747 |
| [TakeutiZaring] p. 35 | Notation | wtr 4887 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | trelpss 39182 tz7.2 5234 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4891 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 5878 |
| [TakeutiZaring] p. 36 | Proposition 7.5 | tz7.5 5886 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 5887 ordelordALT 39270 ordelordALTVD 39623 |
| [TakeutiZaring] p. 37 | Corollary 7.8 | ordelpss 5893 ordelssne 5892 |
| [TakeutiZaring] p. 37 | Proposition 7.7 | tz7.7 5891 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 5895 |
| [TakeutiZaring] p. 38 | Corollary 7.14 | ordeleqon 7139 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 7140 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 5869 |
| [TakeutiZaring] p. 38 | Proposition 7.10 | ordtri3or 5897 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | onfrALT 39287 ordon 7133 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 7135 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 7204 |
| [TakeutiZaring] p. 40 | Exercise 3 | ontr2 5914 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4889 |
| [TakeutiZaring] p. 40 | Exercise 9 | onssmin 7148 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 7182 |
| [TakeutiZaring] p. 40 | Exercise 12 | ordun 5971 |
| [TakeutiZaring] p. 40 | Exercise 14 | ordequn 5970 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 7136 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 4604 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 5871 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 5944 sucidg 5945 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 7164 |
| [TakeutiZaring] p. 41 | Proposition 7.25 | onnbtwn 5960 ordnbtwn 5958 |
| [TakeutiZaring] p. 41 | Proposition 7.26 | onsucuni 7179 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-lim 5870 |
| [TakeutiZaring] p. 42 | Exercise 4 | omssnlim 7230 |
| [TakeutiZaring] p. 42 | Exercise 7 | ssnlim 7234 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 7192 ordelsuc 7171 |
| [TakeutiZaring] p. 42 | Exercise 9 | ordsucelsuc 7173 |
| [TakeutiZaring] p. 42 | Definition 7.27 | nlimon 7202 |
| [TakeutiZaring] p. 42 | Definition 7.28 | dfom2 7218 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 7236 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 7237 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 7238 |
| [TakeutiZaring] p. 43 | Remark | omon 7227 |
| [TakeutiZaring] p. 43 | Axiom 7 | inf3 8700 omex 8708 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 7225 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 7242 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 7239 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 7240 |
| [TakeutiZaring] p. 44 | Exercise 1 | limomss 7221 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 4626 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintss 4903 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 4627 |
| [TakeutiZaring] p. 44 | Exercise 5 | intex 4952 |
| [TakeutiZaring] p. 44 | Exercise 6 | oninton 7151 |
| [TakeutiZaring] p. 44 | Exercise 11 | ordintdif 5916 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 4613 |
| [TakeutiZaring] p. 44 | Proposition 7.34 | noinfep 8725 |
| [TakeutiZaring] p. 45 | Exercise 4 | onint 7146 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 7629 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfr1 7650 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfr2 7651 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfr3 7652 |
| [TakeutiZaring] p. 49 | Theorem 7.44 | tz7.44-1 7659 tz7.44-2 7660 tz7.44-3 7661 |
| [TakeutiZaring] p. 50 | Exercise 1 | smogt 7621 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 7616 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 7600 |
| [TakeutiZaring] p. 51 | Proposition 7.49 | tz7.49 7697 tz7.49c 7698 |
| [TakeutiZaring] p. 51 | Proposition 7.48(1) | tz7.48-1 7695 |
| [TakeutiZaring] p. 51 | Proposition 7.48(2) | tz7.48-2 7694 |
| [TakeutiZaring] p. 51 | Proposition 7.48(3) | tz7.48-3 7696 |
| [TakeutiZaring] p. 53 | Proposition 7.53 | 2eu5 2706 |
| [TakeutiZaring] p. 54 | Proposition 7.56(1) | leweon 9038 |
| [TakeutiZaring] p. 54 | Proposition 7.58(1) | r0weon 9039 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oalim 7770 oasuc 7762 |
| [TakeutiZaring] p. 57 | Remark | tfindsg 7211 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 7773 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 7754 oa0r 7776 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 7774 |
| [TakeutiZaring] p. 58 | Corollary 8.5 | oacan 7786 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 7857 nnaordi 7856 oaord 7785 oaordi 7784 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4700 uniss2 4607 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordri 7788 |
| [TakeutiZaring] p. 59 | Proposition 8.8 | oawordeu 7793 oawordex 7795 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 7849 |
| [TakeutiZaring] p. 59 | Proposition 8.10 | oaabs 7882 |
| [TakeutiZaring] p. 60 | Remark | oancom 8716 |
| [TakeutiZaring] p. 60 | Proposition 8.11 | oalimcl 7798 |
| [TakeutiZaring] p. 62 | Exercise 1 | nnarcl 7854 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 7790 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 7755 om0x 7757 omlim 7771 omsuc 7764 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnecl 7851 nnmcl 7850 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 7870 nnmordi 7869 omord 7806 omordi 7804 |
| [TakeutiZaring] p. 63 | Proposition 8.20 | omcan 7807 |
| [TakeutiZaring] p. 63 | Proposition 8.21 | nnmwordri 7874 omwordri 7810 |
| [TakeutiZaring] p. 63 | Proposition 8.18(1) | om0r 7777 |
| [TakeutiZaring] p. 63 | Proposition 8.18(2) | om1 7780 om1r 7781 |
| [TakeutiZaring] p. 64 | Proposition 8.22 | om00 7813 |
| [TakeutiZaring] p. 64 | Proposition 8.23 | omordlim 7815 |
| [TakeutiZaring] p. 64 | Proposition 8.24 | omlimcl 7816 |
| [TakeutiZaring] p. 64 | Proposition 8.25 | odi 7817 |
| [TakeutiZaring] p. 65 | Theorem 8.26 | omass 7818 |
| [TakeutiZaring] p. 67 | Definition 8.30 | nnesuc 7846 oe0 7760 oelim 7772 oesuc 7765 onesuc 7768 |
| [TakeutiZaring] p. 67 | Proposition 8.31 | oe0m0 7758 |
| [TakeutiZaring] p. 67 | Proposition 8.32 | oen0 7824 |
| [TakeutiZaring] p. 67 | Proposition 8.33 | oeordi 7825 |
| [TakeutiZaring] p. 67 | Proposition 8.31(2) | oe0m1 7759 |
| [TakeutiZaring] p. 67 | Proposition 8.31(3) | oe1m 7783 |
| [TakeutiZaring] p. 68 | Corollary 8.34 | oeord 7826 |
| [TakeutiZaring] p. 68 | Corollary 8.36 | oeordsuc 7832 |
| [TakeutiZaring] p. 68 | Proposition 8.35 | oewordri 7830 |
| [TakeutiZaring] p. 68 | Proposition 8.37 | oeworde 7831 |
| [TakeutiZaring] p. 69 | Proposition 8.41 | oeoa 7835 |
| [TakeutiZaring] p. 70 | Proposition 8.42 | oeoe 7837 |
| [TakeutiZaring] p. 73 | Theorem 9.1 | trcl 8772 tz9.1 8773 |
| [TakeutiZaring] p. 76 | Definition 9.9 | df-r1 8795 r10 8799 r1lim 8803 r1limg 8802 r1suc 8801 r1sucg 8800 |
| [TakeutiZaring] p. 77 | Proposition 9.10(2) | r1ord 8811 r1ord2 8812 r1ordg 8809 |
| [TakeutiZaring] p. 78 | Proposition 9.12 | tz9.12 8821 |
| [TakeutiZaring] p. 78 | Proposition 9.13 | rankwflem 8846 tz9.13 8822 tz9.13g 8823 |
| [TakeutiZaring] p. 79 | Definition 9.14 | df-rank 8796 rankval 8847 rankvalb 8828 rankvalg 8848 |
| [TakeutiZaring] p. 79 | Proposition 9.16 | rankel 8870 rankelb 8855 |
| [TakeutiZaring] p. 79 | Proposition 9.17 | rankuni2b 8884 rankval3 8871 rankval3b 8857 |
| [TakeutiZaring] p. 79 | Proposition 9.18 | rankonid 8860 |
| [TakeutiZaring] p. 79 | Proposition 9.15(1) | rankon 8826 |
| [TakeutiZaring] p. 79 | Proposition 9.15(2) | rankr1 8865 rankr1c 8852 rankr1g 8863 |
| [TakeutiZaring] p. 79 | Proposition 9.15(3) | ssrankr1 8866 |
| [TakeutiZaring] p. 80 | Exercise 1 | rankss 8880 rankssb 8879 |
| [TakeutiZaring] p. 80 | Exercise 2 | unbndrank 8873 |
| [TakeutiZaring] p. 80 | Proposition 9.19 | bndrank 8872 |
| [TakeutiZaring] p. 83 | Axiom of Choice | ac4 9503 dfac3 9148 |
| [TakeutiZaring] p. 84 | Theorem 10.3 | dfac8a 9057 numth 9500 numth2 9499 |
| [TakeutiZaring] p. 85 | Definition 10.4 | cardval 9574 |
| [TakeutiZaring] p. 85 | Proposition 10.5 | cardid 9575 cardid2 8983 |
| [TakeutiZaring] p. 85 | Proposition 10.9 | oncard 8990 |
| [TakeutiZaring] p. 85 | Proposition 10.10 | carden 9579 |
| [TakeutiZaring] p. 85 | Proposition 10.11 | cardidm 8989 |
| [TakeutiZaring] p. 85 | Proposition 10.6(1) | cardon 8974 |
| [TakeutiZaring] p. 85 | Proposition 10.6(2) | cardne 8995 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 8987 |
| [TakeutiZaring] p. 87 | Proposition 10.15 | pwen 8293 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 8176 |
| [TakeutiZaring] p. 88 | Exercise 7 | infensuc 8298 |
| [TakeutiZaring] p. 89 | Exercise 10 | omxpen 8222 |
| [TakeutiZaring] p. 90 | Corollary 10.23 | cardnn 8993 |
| [TakeutiZaring] p. 90 | Definition 10.27 | alephiso 9125 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 8303 |
| [TakeutiZaring] p. 90 | Proposition 10.22 | onomeneq 8310 |
| [TakeutiZaring] p. 90 | Proposition 10.26 | alephprc 9126 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 8308 |
| [TakeutiZaring] p. 91 | Exercise 2 | alephle 9115 |
| [TakeutiZaring] p. 91 | Exercise 3 | aleph0 9093 |
| [TakeutiZaring] p. 91 | Exercise 4 | cardlim 9002 |
| [TakeutiZaring] p. 91 | Exercise 7 | infpss 9245 |
| [TakeutiZaring] p. 91 | Exercise 8 | infcntss 8394 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 8117 isfi 8137 |
| [TakeutiZaring] p. 92 | Proposition 10.32 | onfin 8311 |
| [TakeutiZaring] p. 92 | Proposition 10.34 | imadomg 9562 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 8215 |
| [TakeutiZaring] p. 93 | Proposition 10.35 | fodomb 9554 |
| [TakeutiZaring] p. 93 | Proposition 10.36 | cdaxpdom 9217 unxpdom 8327 |
| [TakeutiZaring] p. 93 | Proposition 10.37 | cardsdomel 9004 cardsdomelir 9003 |
| [TakeutiZaring] p. 93 | Proposition 10.38 | sucxpdom 8329 |
| [TakeutiZaring] p. 94 | Proposition 10.39 | infxpen 9041 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 8015 |
| [TakeutiZaring] p. 95 | Proposition 10.40 | infxpidm 9590 infxpidm2 9044 |
| [TakeutiZaring] p. 95 | Proposition 10.41 | infcda 9236 infxp 9243 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2en 8227 pw2f1o 8225 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 8286 |
| [TakeutiZaring] p. 97 | Theorem 10.46 | ac6s3 9515 |
| [TakeutiZaring] p. 98 | Theorem 10.46 | ac6c5 9510 ac6s5 9519 |
| [TakeutiZaring] p. 98 | Theorem 10.47 | unidom 9571 |
| [TakeutiZaring] p. 99 | Theorem 10.48 | uniimadom 9572 uniimadomf 9573 |
| [TakeutiZaring] p. 100 | Definition 11.1 | cfcof 9302 |
| [TakeutiZaring] p. 101 | Proposition 11.7 | cofsmo 9297 |
| [TakeutiZaring] p. 102 | Exercise 1 | cfle 9282 |
| [TakeutiZaring] p. 102 | Exercise 2 | cf0 9279 |
| [TakeutiZaring] p. 102 | Exercise 3 | cfsuc 9285 |
| [TakeutiZaring] p. 102 | Exercise 4 | cfom 9292 |
| [TakeutiZaring] p. 102 | Proposition 11.9 | coftr 9301 |
| [TakeutiZaring] p. 103 | Theorem 11.15 | alephreg 9610 |
| [TakeutiZaring] p. 103 | Proposition 11.11 | cardcf 9280 |
| [TakeutiZaring] p. 103 | Proposition 11.13 | alephsing 9304 |
| [TakeutiZaring] p. 104 | Corollary 11.17 | cardinfima 9124 |
| [TakeutiZaring] p. 104 | Proposition 11.16 | carduniima 9123 |
| [TakeutiZaring] p. 104 | Proposition 11.18 | alephfp 9135 alephfp2 9136 |
| [TakeutiZaring] p. 106 | Theorem 11.20 | gchina 9727 |
| [TakeutiZaring] p. 106 | Theorem 11.21 | mappwen 9139 |
| [TakeutiZaring] p. 107 | Theorem 11.26 | konigth 9597 |
| [TakeutiZaring] p. 108 | Theorem 11.28 | pwcfsdom 9611 |
| [TakeutiZaring] p. 108 | Theorem 11.29 | cfpwsdom 9612 |
| [Tarski] p. 67 | Axiom B5 | ax-c5 34689 |
| [Tarski] p. 67 | Scheme B5 | sp 2207 |
| [Tarski] p. 68 | Lemma 6 | avril1 27661 equid 2097 |
| [Tarski] p. 69 | Lemma 7 | equcomi 2102 |
| [Tarski] p. 70 | Lemma 14 | spim 2416 spime 2418 spimeh 2083 |
| [Tarski] p. 70 | Lemma 16 | ax-12 2203 ax-c15 34695 ax12i 2048 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 2272 |
| [Tarski] p. 75 | Axiom B7 | ax6v 2058 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-5 1991 ax5ALT 34713 |
| [Tarski], p. 75 | Scheme B8 of system S2 | ax-7 2093 ax-8 2147 ax-9 2154 |
| [Tarski1999] p. 178 | Axiom 4 | axtgsegcon 25584 |
| [Tarski1999] p. 178 | Axiom 5 | axtg5seg 25585 |
| [Tarski1999] p. 179 | Axiom 7 | axtgpasch 25587 |
| [Tarski1999] p. 180 | Axiom 7.1 | axtgpasch 25587 |
| [Tarski1999] p. 185 | Axiom 11 | axtgcont1 25588 |
| [Truss] p. 114 | Theorem 5.18 | ruc 15178 |
| [Viaclovsky7] p. 3 | Corollary 0.3 | mblfinlem3 33780 |
| [Viaclovsky8] p. 3 | Proposition 7 | ismblfin 33782 |
| [Weierstrass] p. 272 | Definition | df-mdet 20609 mdetuni 20646 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 | pm1.2 889 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 857 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 858 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 905 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 952 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 180 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 132 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 90 wl-pm2.04 33605 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | frege5 38618 imim2 58 wl-imim2 33600 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 83 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1 882 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2712 syl 17 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 888 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 22 wl-id 33603 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmid 880 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 138 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13 883 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotr 128 notnotrALT2 39683 wl-notnotr 33604 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1 145 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | ax-frege28 38648 axfrege28 38647 con3 150 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | ax-3 8 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18 123 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 856 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 910 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 121 wl-pm2.21 33597 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 122 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25 876 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26 925 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | conventions-label 27600 pm2.27 42 wl-pm2.27 33595 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 908 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 909 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 954 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 955 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 953 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1072 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 892 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 893 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 928 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 56 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 868 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 869 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5 165 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6 182 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 870 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 871 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 872 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 166 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 168 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 840 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54 841 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 875 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 877 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61 183 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 885 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 926 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 927 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 184 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 878 pm2.67 879 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521 167 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 884 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 957 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68 886 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinv 194 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 958 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 959 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 919 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 917 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 956 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 960 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 84 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85 918 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 109 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 976 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 455 pm3.2im 158 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11 977 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12 978 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13 979 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 980 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 457 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 447 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 389 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 804 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 435 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 436 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 468 simplim 164 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 471 simprim 163 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 748 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 749 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 809 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 608 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 811 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 480 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 481 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 945 pm3.44 944 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | prth 810 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 459 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 948 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34b 305 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 251 |
| [WhiteheadRussell] p. 117 | Theorem *4.11 | notbi 308 |
| [WhiteheadRussell] p. 117 | Theorem *4.12 | con2bi 342 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotb 304 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14 808 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 828 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 212 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 807 bitr 806 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 553 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 890 pm4.25 891 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 448 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 992 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 859 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 454 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 907 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 617 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 903 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 619 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 961 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1073 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 990 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42 1040 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 1008 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 981 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 983 pm4.45 982 pm4.45im 825 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anor 967 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imor 842 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 535 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianor 966 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52 969 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53 970 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54 971 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55 972 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 968 pm4.56 973 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | oran 974 pm4.57 975 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | pm4.61 391 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62 845 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63 384 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64 838 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65 392 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66 839 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67 385 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 547 pm4.71d 551 pm4.71i 549 pm4.71r 548 pm4.71rd 552 pm4.71ri 550 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 934 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 517 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 922 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 507 pm4.76 508 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 946 pm4.77 947 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78 920 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79 988 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 379 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81 380 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 1009 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83 1010 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 336 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 337 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 340 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 375 impexp 437 pm4.87 832 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 821 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11 929 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12 930 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13 932 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14 931 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15 998 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 999 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17 997 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbn 372 pm5.18 370 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 374 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 822 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xor 1000 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3 1034 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24 1036 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2 887 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 562 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 376 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 350 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6 986 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7 938 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 827 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 563 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 831 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 823 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 829 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 377 pm5.41 378 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 533 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 532 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 989 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54 1003 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55 933 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 985 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62 1004 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63 1005 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71 1014 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 355 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 259 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 1015 |
| [WhiteheadRussell] p. 146 | Theorem *10.12 | pm10.12 39081 |
| [WhiteheadRussell] p. 146 | Theorem *10.14 | pm10.14 39082 |
| [WhiteheadRussell] p. 147 | Theorem *10.22 | 19.26 1949 |
| [WhiteheadRussell] p. 149 | Theorem *10.251 | pm10.251 39083 |
| [WhiteheadRussell] p. 149 | Theorem *10.252 | pm10.252 39084 |
| [WhiteheadRussell] p. 149 | Theorem *10.253 | pm10.253 39085 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1972 |
| [WhiteheadRussell] p. 151 | Theorem *10.301 | albitr 39086 |
| [WhiteheadRussell] p. 155 | Theorem *10.42 | pm10.42 39087 |
| [WhiteheadRussell] p. 155 | Theorem *10.52 | pm10.52 39088 |
| [WhiteheadRussell] p. 155 | Theorem *10.53 | pm10.53 39089 |
| [WhiteheadRussell] p. 155 | Theorem *10.541 | pm10.541 39090 |
| [WhiteheadRussell] p. 156 | Theorem *10.55 | pm10.55 39092 |
| [WhiteheadRussell] p. 156 | Theorem *10.56 | pm10.56 39093 |
| [WhiteheadRussell] p. 156 | Theorem *10.57 | pm10.57 39094 |
| [WhiteheadRussell] p. 156 | Theorem *10.542 | pm10.542 39091 |
| [WhiteheadRussell] p. 159 | Axiom *11.07 | pm11.07 2595 |
| [WhiteheadRussell] p. 159 | Theorem *11.11 | pm11.11 39097 |
| [WhiteheadRussell] p. 159 | Theorem *11.12 | pm11.12 39098 |
| [WhiteheadRussell] p. 159 | Theorem PM*11.1 | 2stdpc4 2500 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 2194 |
| [WhiteheadRussell] p. 160 | Theorem *11.22 | 2exnaln 1904 |
| [WhiteheadRussell] p. 160 | Theorem *11.25 | 2nexaln 1905 |
| [WhiteheadRussell] p. 161 | Theorem *11.3 | 19.21vv 39099 |
| [WhiteheadRussell] p. 162 | Theorem *11.32 | 2alim 39100 |
| [WhiteheadRussell] p. 162 | Theorem *11.33 | 2albi 39101 |
| [WhiteheadRussell] p. 162 | Theorem *11.34 | 2exim 39102 |
| [WhiteheadRussell] p. 162 | Theorem *11.36 | spsbce-2 39104 |
| [WhiteheadRussell] p. 162 | Theorem *11.341 | 2exbi 39103 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1966 |
| [WhiteheadRussell] p. 163 | Theorem *11.43 | 19.36vv 39106 |
| [WhiteheadRussell] p. 163 | Theorem *11.44 | 19.31vv 39107 |
| [WhiteheadRussell] p. 163 | Theorem *11.421 | 19.33-2 39105 |
| [WhiteheadRussell] p. 164 | Theorem *11.5 | 2nalexn 1903 |
| [WhiteheadRussell] p. 164 | Theorem *11.46 | 19.37vv 39108 |
| [WhiteheadRussell] p. 164 | Theorem *11.47 | 19.28vv 39109 |
| [WhiteheadRussell] p. 164 | Theorem *11.51 | 2exnexn 1922 |
| [WhiteheadRussell] p. 164 | Theorem *11.52 | pm11.52 39110 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 2341 |
| [WhiteheadRussell] p. 164 | Theorem *11.521 | 2exanali 39111 |
| [WhiteheadRussell] p. 165 | Theorem *11.6 | pm11.6 39116 |
| [WhiteheadRussell] p. 165 | Theorem *11.56 | aaanv 39112 |
| [WhiteheadRussell] p. 165 | Theorem *11.57 | pm11.57 39113 |
| [WhiteheadRussell] p. 165 | Theorem *11.58 | pm11.58 39114 |
| [WhiteheadRussell] p. 165 | Theorem *11.59 | pm11.59 39115 |
| [WhiteheadRussell] p. 166 | Theorem *11.7 | pm11.7 39120 |
| [WhiteheadRussell] p. 166 | Theorem *11.61 | pm11.61 39117 |
| [WhiteheadRussell] p. 166 | Theorem *11.62 | pm11.62 39118 |
| [WhiteheadRussell] p. 166 | Theorem *11.63 | pm11.63 39119 |
| [WhiteheadRussell] p. 166 | Theorem *11.71 | pm11.71 39121 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2622 |
| [WhiteheadRussell] p. 178 | Theorem *13.13 | pm13.13a 39132 pm13.13b 39133 |
| [WhiteheadRussell] p. 178 | Theorem *13.14 | pm13.14 39134 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 3024 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 3025 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 3495 |
| [WhiteheadRussell] p. 179 | Theorem *13.21 | 2sbc6g 39140 |
| [WhiteheadRussell] p. 179 | Theorem *13.22 | 2sbc5g 39141 |
| [WhiteheadRussell] p. 179 | Theorem *13.192 | pm13.192 39135 |
| [WhiteheadRussell] p. 179 | Theorem *13.193 | 2pm13.193 39291 pm13.193 39136 |
| [WhiteheadRussell] p. 179 | Theorem *13.194 | pm13.194 39137 |
| [WhiteheadRussell] p. 179 | Theorem *13.195 | pm13.195 39138 |
| [WhiteheadRussell] p. 179 | Theorem *13.196 | pm13.196a 39139 |
| [WhiteheadRussell] p. 184 | Theorem *14.12 | pm14.12 39146 |
| [WhiteheadRussell] p. 184 | Theorem *14.111 | iotasbc2 39145 |
| [WhiteheadRussell] p. 184 | Definition *14.01 | iotasbc 39144 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3640 |
| [WhiteheadRussell] p. 185 | Theorem *14.122 | pm14.122a 39147 pm14.122b 39148 pm14.122c 39149 |
| [WhiteheadRussell] p. 185 | Theorem *14.123 | pm14.123a 39150 pm14.123b 39151 pm14.123c 39152 |
| [WhiteheadRussell] p. 189 | Theorem *14.2 | iotaequ 39154 |
| [WhiteheadRussell] p. 189 | Theorem *14.18 | pm14.18 39153 |
| [WhiteheadRussell] p. 189 | Theorem *14.202 | iotavalb 39155 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 6011 |
| [WhiteheadRussell] p. 190 | Theorem *14.205 | iotasbc5 39156 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 6012 |
| [WhiteheadRussell] p. 191 | Theorem *14.24 | pm14.24 39157 |
| [WhiteheadRussell] p. 192 | Theorem *14.25 | sbiota1 39159 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2685 eupickbi 2688 sbaniota 39160 |
| [WhiteheadRussell] p. 192 | Theorem *14.242 | iotavalsb 39158 |
| [WhiteheadRussell] p. 192 | Theorem *14.271 | eubi 39161 |
| [WhiteheadRussell] p. 193 | Theorem *14.272 | iotasbcq 39162 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | conventions 27599 df-fv 6038 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 9030 pm54.43lem 9029 |
| [Young] p. 141 | Definition of operator ordering | leop2 29323 |
| [Young] p. 142 | Example 12.2(i) | 0leop 29329 idleop 29330 |
| [vandenDries] p. 42 | Lemma 61 | irrapx1 37916 |
| [vandenDries] p. 43 | Theorem 62 | pellex 37923 pellexlem1 37917 |