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 16329 |
| [Adamek] p. 21 | Condition 3.1(b) | df-cat 16329 |
| [Adamek] p. 22 | Example 3.3(1) | df-setc 16726 |
| [Adamek] p. 24 | Example 3.3(4.c) | 0cat 16349 |
| [Adamek] p. 25 | Definition 3.5 | df-oppc 16372 |
| [Adamek] p. 28 | Remark 3.9 | oppciso 16441 |
| [Adamek] p. 28 | Remark 3.12 | invf1o 16429 invisoinvl 16450 |
| [Adamek] p. 28 | Example 3.13 | idinv 16449 idiso 16448 |
| [Adamek] p. 28 | Corollary 3.11 | inveq 16434 |
| [Adamek] p. 28 | Definition 3.8 | df-inv 16408 df-iso 16409 dfiso2 16432 |
| [Adamek] p. 28 | Proposition 3.10 | sectcan 16415 |
| [Adamek] p. 29 | Remark 3.16 | cicer 16466 |
| [Adamek] p. 29 | Definition 3.15 | cic 16459 df-cic 16456 |
| [Adamek] p. 29 | Definition 3.17 | df-func 16518 |
| [Adamek] p. 29 | Proposition 3.14(1) | invinv 16430 |
| [Adamek] p. 29 | Proposition 3.14(2) | invco 16431 isoco 16437 |
| [Adamek] p. 30 | Remark 3.19 | df-func 16518 |
| [Adamek] p. 30 | Example 3.20(1) | idfucl 16541 |
| [Adamek] p. 32 | Proposition 3.21 | funciso 16534 |
| [Adamek] p. 33 | Proposition 3.23 | cofucl 16548 |
| [Adamek] p. 34 | Remark 3.28(2) | catciso 16757 |
| [Adamek] p. 34 | Remark 3.28 (1) | embedsetcestrc 16807 |
| [Adamek] p. 34 | Definition 3.27(2) | df-fth 16565 |
| [Adamek] p. 34 | Definition 3.27(3) | df-full 16564 |
| [Adamek] p. 34 | Definition 3.27 (1) | embedsetcestrc 16807 |
| [Adamek] p. 35 | Corollary 3.32 | ffthiso 16589 |
| [Adamek] p. 35 | Proposition 3.30(c) | cofth 16595 |
| [Adamek] p. 35 | Proposition 3.30(d) | cofull 16594 |
| [Adamek] p. 36 | Definition 3.33 (1) | equivestrcsetc 16792 |
| [Adamek] p. 36 | Definition 3.33 (2) | equivestrcsetc 16792 |
| [Adamek] p. 39 | Definition 3.41 | funcoppc 16535 |
| [Adamek] p. 39 | Definition 3.44. | df-catc 16745 |
| [Adamek] p. 39 | Proposition 3.43(c) | fthoppc 16583 |
| [Adamek] p. 39 | Proposition 3.43(d) | fulloppc 16582 |
| [Adamek] p. 40 | Remark 3.48 | catccat 16754 |
| [Adamek] p. 40 | Definition 3.47 | df-catc 16745 |
| [Adamek] p. 48 | Example 4.3(1.a) | 0subcat 16498 |
| [Adamek] p. 48 | Example 4.3(1.b) | catsubcat 16499 |
| [Adamek] p. 48 | Definition 4.1(2) | fullsubc 16510 |
| [Adamek] p. 48 | Definition 4.1(a) | df-subc 16472 |
| [Adamek] p. 49 | Remark 4.4(2) | ressffth 16598 |
| [Adamek] p. 83 | Definition 6.1 | df-nat 16603 |
| [Adamek] p. 87 | Remark 6.14(a) | fuccocl 16624 |
| [Adamek] p. 87 | Remark 6.14(b) | fucass 16628 |
| [Adamek] p. 87 | Definition 6.15 | df-fuc 16604 |
| [Adamek] p. 88 | Remark 6.16 | fuccat 16630 |
| [Adamek] p. 101 | Definition 7.1 | df-inito 16641 |
| [Adamek] p. 101 | Example 7.2 (6) | irinitoringc 42069 |
| [Adamek] p. 102 | Definition 7.4 | df-termo 16642 |
| [Adamek] p. 102 | Proposition 7.3 (1) | initoeu1w 16662 |
| [Adamek] p. 102 | Proposition 7.3 (2) | initoeu2 16666 |
| [Adamek] p. 103 | Definition 7.7 | df-zeroo 16643 |
| [Adamek] p. 103 | Example 7.9 (3) | nzerooringczr 42072 |
| [Adamek] p. 103 | Proposition 7.6 | termoeu1w 16669 |
| [Adamek] p. 106 | Definition 7.19 | df-sect 16407 |
| [Adamek] p. 478 | Item Rng | df-ringc 42005 |
| [AhoHopUll] p. 2 | Section 1.1 | df-bigo 42342 |
| [AhoHopUll] p. 12 | Section 1.3 | df-blen 42364 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 13301 df-pfx 41382 df-substr 13303 df-word 13299 lencl 13324 wrd0 13330 |
| [AkhiezerGlazman] p. 39 | Linear operator norm | df-nmo 22512 df-nmoo 27600 |
| [AkhiezerGlazman] p. 64 | Theorem | hmopidmch 29012 hmopidmchi 29010 |
| [AkhiezerGlazman] p. 65 | Theorem 1 | pjcmul1i 29060 pjcmul2i 29061 |
| [AkhiezerGlazman] p. 72 | Theorem | cnvunop 28777 unoplin 28779 |
| [AkhiezerGlazman] p. 72 | Equation 2 | unopadj 28778 unopadj2 28797 |
| [AkhiezerGlazman] p. 73 | Theorem | elunop2 28872 lnopunii 28871 |
| [AkhiezerGlazman] p. 80 | Proposition 1 | adjlnop 28945 |
| [Apostol] p. 18 | Theorem I.1 | addcan 10220 addcan2d 10240 addcan2i 10230 addcand 10239 addcani 10229 |
| [Apostol] p. 18 | Theorem I.2 | negeu 10271 |
| [Apostol] p. 18 | Theorem I.3 | negsub 10329 negsubd 10398 negsubi 10359 |
| [Apostol] p. 18 | Theorem I.4 | negneg 10331 negnegd 10383 negnegi 10351 |
| [Apostol] p. 18 | Theorem I.5 | subdi 10463 subdid 10486 subdii 10479 subdir 10464 subdird 10487 subdiri 10480 |
| [Apostol] p. 18 | Theorem I.6 | mul01 10215 mul01d 10235 mul01i 10226 mul02 10214 mul02d 10234 mul02i 10225 |
| [Apostol] p. 18 | Theorem I.7 | mulcan 10664 mulcan2d 10661 mulcand 10660 mulcani 10666 |
| [Apostol] p. 18 | Theorem I.8 | receu 10672 xreceu 29630 |
| [Apostol] p. 18 | Theorem I.9 | divrec 10701 divrecd 10804 divreci 10770 divreczi 10763 |
| [Apostol] p. 18 | Theorem I.10 | recrec 10722 recreci 10757 |
| [Apostol] p. 18 | Theorem I.11 | mul0or 10667 mul0ord 10677 mul0ori 10675 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 10469 mul2negd 10485 mul2negi 10478 mulneg1 10466 mulneg1d 10483 mulneg1i 10476 |
| [Apostol] p. 18 | Theorem I.13 | divadddiv 10740 divadddivd 10845 divadddivi 10787 |
| [Apostol] p. 18 | Theorem I.14 | divmuldiv 10725 divmuldivd 10842 divmuldivi 10785 rdivmuldivd 29791 |
| [Apostol] p. 18 | Theorem I.15 | divdivdiv 10726 divdivdivd 10848 divdivdivi 10788 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 11854 rpaddcld 11887 rpmulcl 11855 rpmulcld 11888 |
| [Apostol] p. 20 | Axiom 8 | rpneg 11863 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 11865 |
| [Apostol] p. 20 | Theorem I.17 | lttri 10163 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 10620 ltadd1dd 10638 ltadd1i 10582 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 10873 ltmul1a 10872 ltmul1i 10942 ltmul1ii 10952 ltmul2 10874 ltmul2d 11914 ltmul2dd 11928 ltmul2i 10945 |
| [Apostol] p. 20 | Theorem I.20 | msqgt0 10548 msqgt0d 10595 msqgt0i 10565 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 10550 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 10534 lt0neg1d 10597 ltneg 10528 ltnegd 10605 ltnegi 10572 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 10513 lt2addd 10650 lt2addi 10590 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 11833 |
| [Apostol] p. 21 | Exercise 4 | recgt0 10867 recgt0d 10958 recgt0i 10928 recgt0ii 10929 |
| [Apostol] p. 22 | Definition of integers | df-z 11378 |
| [Apostol] p. 22 | Definition of positive integers | dfnn3 11034 |
| [Apostol] p. 22 | Definition of rationals | df-q 11789 |
| [Apostol] p. 24 | Theorem I.26 | supeu 8360 |
| [Apostol] p. 26 | Theorem I.28 | nnunb 11288 |
| [Apostol] p. 26 | Theorem I.29 | arch 11289 |
| [Apostol] p. 28 | Exercise 2 | btwnz 11479 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 11290 |
| [Apostol] p. 28 | Exercise 4 | rebtwnz 11787 |
| [Apostol] p. 28 | Exercise 5 | zbtwnre 11786 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 12030 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 15063 zneo 11460 zneoALTV 41580 |
| [Apostol] p. 29 | Theorem I.35 | msqsqrtd 14179 resqrtth 13996 sqrtth 14104 sqrtthi 14110 sqsqrtd 14178 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 11023 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwo 11753 |
| [Apostol] p. 361 | Remark | crreczi 12989 |
| [Apostol] p. 363 | Remark | absgt0i 14138 |
| [Apostol] p. 363 | Example | abssubd 14192 abssubi 14142 |
| [ApostolNT] p. 7 | Remark | fmtno0 41452 fmtno1 41453 fmtno2 41462 fmtno3 41463 fmtno4 41464 fmtno5fac 41494 fmtnofz04prm 41489 |
| [ApostolNT] p. 7 | Definition | df-fmtno 41440 |
| [ApostolNT] p. 8 | Definition | df-ppi 24826 |
| [ApostolNT] p. 14 | Definition | df-dvds 14984 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 14995 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 15018 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 15014 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 15008 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 15010 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 14996 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 14997 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 15002 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 15033 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 15035 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 15037 |
| [ApostolNT] p. 15 | Definition | df-gcd 15217 dfgcd2 15263 |
| [ApostolNT] p. 16 | Definition | isprm2 15395 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 15366 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 15619 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 15235 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 15264 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 15266 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 15249 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 15241 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 15423 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 15425 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 15632 |
| [ApostolNT] p. 18 | Theorem 1.13 | prmrec 15626 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 15126 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 15300 |
| [ApostolNT] p. 24 | Definition | df-mu 24827 |
| [ApostolNT] p. 25 | Definition | df-phi 15471 |
| [ApostolNT] p. 25 | Theorem 2.1 | musum 24917 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 15495 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 15481 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 15485 |
| [ApostolNT] p. 32 | Definition | df-vma 24824 |
| [ApostolNT] p. 32 | Theorem 2.9 | muinv 24919 |
| [ApostolNT] p. 32 | Theorem 2.10 | vmasum 24941 |
| [ApostolNT] p. 38 | Remark | df-sgm 24828 |
| [ApostolNT] p. 38 | Definition | df-sgm 24828 |
| [ApostolNT] p. 75 | Definition | df-chp 24825 df-cht 24823 |
| [ApostolNT] p. 104 | Definition | congr 15378 |
| [ApostolNT] p. 106 | Remark | dvdsval3 14987 |
| [ApostolNT] p. 106 | Definition | moddvds 14991 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 15070 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 15071 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 12687 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modmul12d 12724 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modexp 12999 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 15013 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 15381 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 15778 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 15383 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 15488 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 15506 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 15489 |
| [ApostolNT] p. 116 | Theorem 5.24 | wilthimp 24798 |
| [ApostolNT] p. 179 | Definition | df-lgs 25020 lgsprme0 25064 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 25065 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 25041 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 25056 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 25113 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 25132 2lgsoddprm 25141 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 25099 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 25108 |
| [ApostolNT] p. 188 | Definition | df-lgs 25020 lgs1 25066 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 25057 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 25059 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 25067 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 25068 |
| [Baer] p. 40 | Property (b) | mapdord 36927 |
| [Baer] p. 40 | Property (c) | mapd11 36928 |
| [Baer] p. 40 | Property (e) | mapdin 36951 mapdlsm 36953 |
| [Baer] p. 40 | Property (f) | mapd0 36954 |
| [Baer] p. 40 | Definition of projectivity | df-mapd 36914 mapd1o 36937 |
| [Baer] p. 41 | Property (g) | mapdat 36956 |
| [Baer] p. 44 | Part (1) | mapdpg 36995 |
| [Baer] p. 45 | Part (2) | hdmap1eq 37091 mapdheq 37017 mapdheq2 37018 mapdheq2biN 37019 |
| [Baer] p. 45 | Part (3) | baerlem3 37002 |
| [Baer] p. 46 | Part (4) | mapdheq4 37021 mapdheq4lem 37020 |
| [Baer] p. 46 | Part (5) | baerlem5a 37003 baerlem5abmN 37007 baerlem5amN 37005 baerlem5b 37004 baerlem5bmN 37006 |
| [Baer] p. 47 | Part (6) | hdmap1l6 37111 hdmap1l6a 37099 hdmap1l6e 37104 hdmap1l6f 37105 hdmap1l6g 37106 hdmap1l6lem1 37097 hdmap1l6lem2 37098 hdmap1p6N 37112 mapdh6N 37036 mapdh6aN 37024 mapdh6eN 37029 mapdh6fN 37030 mapdh6gN 37031 mapdh6lem1N 37022 mapdh6lem2N 37023 |
| [Baer] p. 48 | Part 9 | hdmapval 37120 |
| [Baer] p. 48 | Part 10 | hdmap10 37132 |
| [Baer] p. 48 | Part 11 | hdmapadd 37135 |
| [Baer] p. 48 | Part (6) | hdmap1l6h 37107 mapdh6hN 37032 |
| [Baer] p. 48 | Part (7) | mapdh75cN 37042 mapdh75d 37043 mapdh75e 37041 mapdh75fN 37044 mapdh7cN 37038 mapdh7dN 37039 mapdh7eN 37037 mapdh7fN 37040 |
| [Baer] p. 48 | Part (8) | mapdh8 37078 mapdh8a 37064 mapdh8aa 37065 mapdh8ab 37066 mapdh8ac 37067 mapdh8ad 37068 mapdh8b 37069 mapdh8c 37070 mapdh8d 37072 mapdh8d0N 37071 mapdh8e 37073 mapdh8fN 37074 mapdh8g 37075 mapdh8i 37076 mapdh8j 37077 |
| [Baer] p. 48 | Part (9) | mapdh9a 37079 |
| [Baer] p. 48 | Equation 10 | mapdhvmap 37058 |
| [Baer] p. 49 | Part 12 | hdmap11 37140 hdmapeq0 37136 hdmapf1oN 37157 hdmapneg 37138 hdmaprnN 37156 hdmaprnlem1N 37141 hdmaprnlem3N 37142 hdmaprnlem3uN 37143 hdmaprnlem4N 37145 hdmaprnlem6N 37146 hdmaprnlem7N 37147 hdmaprnlem8N 37148 hdmaprnlem9N 37149 hdmapsub 37139 |
| [Baer] p. 49 | Part 14 | hdmap14lem1 37160 hdmap14lem10 37169 hdmap14lem1a 37158 hdmap14lem2N 37161 hdmap14lem2a 37159 hdmap14lem3 37162 hdmap14lem8 37167 hdmap14lem9 37168 |
| [Baer] p. 50 | Part 14 | hdmap14lem11 37170 hdmap14lem12 37171 hdmap14lem13 37172 hdmap14lem14 37173 hdmap14lem15 37174 hgmapval 37179 |
| [Baer] p. 50 | Part 15 | hgmapadd 37186 hgmapmul 37187 hgmaprnlem2N 37189 hgmapvs 37183 |
| [Baer] p. 50 | Part 16 | hgmaprnN 37193 |
| [Baer] p. 110 | Lemma 1 | hdmapip0com 37209 |
| [Baer] p. 110 | Line 27 | hdmapinvlem1 37210 |
| [Baer] p. 110 | Line 28 | hdmapinvlem2 37211 |
| [Baer] p. 110 | Line 30 | hdmapinvlem3 37212 |
| [Baer] p. 110 | Part 1.2 | hdmapglem5 37214 hgmapvv 37218 |
| [Baer] p. 110 | Proposition 1 | hdmapinvlem4 37213 |
| [Baer] p. 111 | Line 10 | hgmapvvlem1 37215 |
| [Baer] p. 111 | Line 15 | hdmapg 37222 hdmapglem7 37221 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 23 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2474 |
| [BellMachover] p. 460 | Notation | df-mo 2475 |
| [BellMachover] p. 460 | Definition | mo3 2507 |
| [BellMachover] p. 461 | Axiom Ext | ax-ext 2602 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2607 |
| [BellMachover] p. 463 | Axiom Rep | axrep5 4776 |
| [BellMachover] p. 463 | Scheme Sep | axsep 4780 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4784 |
| [BellMachover] p. 466 | Problem | axpow2 4845 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4846 |
| [BellMachover] p. 466 | Axiom Union | axun2 6951 |
| [BellMachover] p. 468 | Definition | df-ord 5726 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 5741 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 5748 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 5743 |
| [BellMachover] p. 471 | Definition of N | df-om 7066 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 7006 |
| [BellMachover] p. 471 | Definition of Lim | df-lim 5728 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 8539 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 7080 |
| [BellMachover] p. 477 | Equation 3.1 | df-r1 8627 |
| [BellMachover] p. 478 | Definition | rankval2 8681 |
| [BellMachover] p. 478 | Theorem 3.3(i) | r1ord3 8645 r1ord3g 8642 |
| [BellMachover] p. 480 | Axiom Reg | zfreg 8500 |
| [BellMachover] p. 488 | Axiom AC | ac5 9299 dfac4 8945 |
| [BellMachover] p. 490 | Definition of aleph | alephval3 8933 |
| [BeltramettiCassinelli] p. 98 | Remark | atlatmstc 34606 |
| [BeltramettiCassinelli] p. 107 | Remark 10.3.5 | atom1d 29212 |
| [BeltramettiCassinelli] p. 166 | Theorem 14.8.4 | chirred 29254 chirredi 29253 |
| [BeltramettiCassinelli1] p. 400 | Proposition P8(ii) | atoml2i 29242 |
| [Beran] p. 3 | Definition of join | sshjval3 28213 |
| [Beran] p. 39 | Theorem 2.3(i) | cmcm2 28475 cmcm2i 28452 cmcm2ii 28457 cmt2N 34537 |
| [Beran] p. 40 | Theorem 2.3(iii) | lecm 28476 lecmi 28461 lecmii 28462 |
| [Beran] p. 45 | Theorem 3.4 | cmcmlem 28450 |
| [Beran] p. 49 | Theorem 4.2 | cm2j 28479 cm2ji 28484 cm2mi 28485 |
| [Beran] p. 95 | Definition | df-sh 28064 issh2 28066 |
| [Beran] p. 95 | Lemma 3.1(S5) | his5 27943 |
| [Beran] p. 95 | Lemma 3.1(S6) | his6 27956 |
| [Beran] p. 95 | Lemma 3.1(S7) | his7 27947 |
| [Beran] p. 95 | Lemma 3.2(S8) | ho01i 28687 |
| [Beran] p. 95 | Lemma 3.2(S9) | hoeq1 28689 |
| [Beran] p. 95 | Lemma 3.2(S10) | ho02i 28688 |
| [Beran] p. 95 | Lemma 3.2(S11) | hoeq2 28690 |
| [Beran] p. 95 | Postulate (S1) | ax-his1 27939 his1i 27957 |
| [Beran] p. 95 | Postulate (S2) | ax-his2 27940 |
| [Beran] p. 95 | Postulate (S3) | ax-his3 27941 |
| [Beran] p. 95 | Postulate (S4) | ax-his4 27942 |
| [Beran] p. 96 | Definition of norm | df-hnorm 27825 dfhnorm2 27979 normval 27981 |
| [Beran] p. 96 | Definition for Cauchy sequence | hcau 28041 |
| [Beran] p. 96 | Definition of Cauchy sequence | df-hcau 27830 |
| [Beran] p. 96 | Definition of complete subspace | isch3 28098 |
| [Beran] p. 96 | Definition of converge | df-hlim 27829 hlimi 28045 |
| [Beran] p. 97 | Theorem 3.3(i) | norm-i-i 27990 norm-i 27986 |
| [Beran] p. 97 | Theorem 3.3(ii) | norm-ii-i 27994 norm-ii 27995 normlem0 27966 normlem1 27967 normlem2 27968 normlem3 27969 normlem4 27970 normlem5 27971 normlem6 27972 normlem7 27973 normlem7tALT 27976 |
| [Beran] p. 97 | Theorem 3.3(iii) | norm-iii-i 27996 norm-iii 27997 |
| [Beran] p. 98 | Remark 3.4 | bcs 28038 bcsiALT 28036 bcsiHIL 28037 |
| [Beran] p. 98 | Remark 3.4(B) | normlem9at 27978 normpar 28012 normpari 28011 |
| [Beran] p. 98 | Remark 3.4(C) | normpyc 28003 normpyth 28002 normpythi 27999 |
| [Beran] p. 99 | Remark | lnfn0 28906 lnfn0i 28901 lnop0 28825 lnop0i 28829 |
| [Beran] p. 99 | Theorem 3.5(i) | nmcexi 28885 nmcfnex 28912 nmcfnexi 28910 nmcopex 28888 nmcopexi 28886 |
| [Beran] p. 99 | Theorem 3.5(ii) | nmcfnlb 28913 nmcfnlbi 28911 nmcoplb 28889 nmcoplbi 28887 |
| [Beran] p. 99 | Theorem 3.5(iii) | lnfncon 28915 lnfnconi 28914 lnopcon 28894 lnopconi 28893 |
| [Beran] p. 100 | Lemma 3.6 | normpar2i 28013 |
| [Beran] p. 101 | Lemma 3.6 | norm3adifi 28010 norm3adifii 28005 norm3dif 28007 norm3difi 28004 |
| [Beran] p. 102 | Theorem 3.7(i) | chocunii 28160 pjhth 28252 pjhtheu 28253 pjpjhth 28284 pjpjhthi 28285 pjth 23210 |
| [Beran] p. 102 | Theorem 3.7(ii) | ococ 28265 ococi 28264 |
| [Beran] p. 103 | Remark 3.8 | nlelchi 28920 |
| [Beran] p. 104 | Theorem 3.9 | riesz3i 28921 riesz4 28923 riesz4i 28922 |
| [Beran] p. 104 | Theorem 3.10 | cnlnadj 28938 cnlnadjeu 28937 cnlnadjeui 28936 cnlnadji 28935 cnlnadjlem1 28926 nmopadjlei 28947 |
| [Beran] p. 106 | Theorem 3.11(i) | adjeq0 28950 |
| [Beran] p. 106 | Theorem 3.11(v) | nmopadji 28949 |
| [Beran] p. 106 | Theorem 3.11(ii) | adjmul 28951 |
| [Beran] p. 106 | Theorem 3.11(iv) | adjadj 28795 |
| [Beran] p. 106 | Theorem 3.11(vi) | nmopcoadj2i 28961 nmopcoadji 28960 |
| [Beran] p. 106 | Theorem 3.11(iii) | adjadd 28952 |
| [Beran] p. 106 | Theorem 3.11(vii) | nmopcoadj0i 28962 |
| [Beran] p. 106 | Theorem 3.11(viii) | adjcoi 28959 pjadj2coi 29063 pjadjcoi 29020 |
| [Beran] p. 107 | Definition | df-ch 28078 isch2 28080 |
| [Beran] p. 107 | Remark 3.12 | choccl 28165 isch3 28098 occl 28163 ocsh 28142 shoccl 28164 shocsh 28143 |
| [Beran] p. 107 | Remark 3.12(B) | ococin 28267 |
| [Beran] p. 108 | Theorem 3.13 | chintcl 28191 |
| [Beran] p. 109 | Property (i) | pjadj2 29046 pjadj3 29047 pjadji 28544 pjadjii 28533 |
| [Beran] p. 109 | Property (ii) | pjidmco 29040 pjidmcoi 29036 pjidmi 28532 |
| [Beran] p. 110 | Definition of projector ordering | pjordi 29032 |
| [Beran] p. 111 | Remark | ho0val 28609 pjch1 28529 |
| [Beran] p. 111 | Definition | df-hfmul 28593 df-hfsum 28592 df-hodif 28591 df-homul 28590 df-hosum 28589 |
| [Beran] p. 111 | Lemma 4.4(i) | pjo 28530 |
| [Beran] p. 111 | Lemma 4.4(ii) | pjch 28553 pjchi 28291 |
| [Beran] p. 111 | Lemma 4.4(iii) | pjoc2 28298 pjoc2i 28297 |
| [Beran] p. 112 | Theorem 4.5(i)->(ii) | pjss2i 28539 |
| [Beran] p. 112 | Theorem 4.5(i)->(iv) | pjssmi 29024 pjssmii 28540 |
| [Beran] p. 112 | Theorem 4.5(i)<->(ii) | pjss2coi 29023 |
| [Beran] p. 112 | Theorem 4.5(i)<->(iii) | pjss1coi 29022 |
| [Beran] p. 112 | Theorem 4.5(i)<->(vi) | pjnormssi 29027 |
| [Beran] p. 112 | Theorem 4.5(iv)->(v) | pjssge0i 29025 pjssge0ii 28541 |
| [Beran] p. 112 | Theorem 4.5(v)<->(vi) | pjdifnormi 29026 pjdifnormii 28542 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1701 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1699 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1702 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1697 |
| [Bogachev] p. 16 | Definition 1.5 | df-oms 30354 |
| [Bogachev] p. 17 | Lemma 1.5.4 | omssubadd 30362 |
| [Bogachev] p. 17 | Example 1.5.2 | omsmon 30360 |
| [Bogachev] p. 41 | Definition 1.11.2 | df-carsg 30364 |
| [Bogachev] p. 42 | Theorem 1.11.4 | carsgsiga 30384 |
| [Bogachev] p. 116 | Definition 2.3.1 | df-itgm 30415 df-sitm 30393 |
| [Bogachev] p. 118 | Chapter 2.4.4 | df-itgm 30415 |
| [Bogachev] p. 118 | Definition 2.4.1 | df-sitg 30392 |
| [Bollobas] p. 1 | Section I.1 | df-edg 25940 isuhgrop 25965 isusgrop 26057 isuspgrop 26056 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 26160 uhgrspan1 26195 uhgrspansubgr 26183 |
| [Bollobas] p. 3 | Section I.1 | cusgrsize 26350 df-cusgr 26232 df-nbgr 26228 fusgrmaxsize 26360 |
| [Bollobas] p. 4 | Definition | df-upwlks 41715 df-wlks 26495 |
| [Bollobas] p. 4 | Section I.1 | finsumvtxdg2size 26446 finsumvtxdgeven 26448 fusgr1th 26447 fusgrvtxdgonume 26450 vtxdgoddnumeven 26449 |
| [Bollobas] p. 5 | Notation | df-pths 26612 |
| [Bollobas] p. 5 | Definition | df-crcts 26681 df-cycls 26682 df-trls 26589 df-wlkson 26496 |
| [Bollobas] p. 7 | Section I.1 | df-ushgr 25954 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-clintop 41836 df-cllaw 41822 df-mgm 17242 df-mgm2 41855 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-assintop 41837 df-asslaw 41824 df-sgrp 17284 df-sgrp2 41857 |
| [BourbakiAlg1] p. 7 | Definition 8 | df-cmgm2 41856 df-comlaw 41823 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 17295 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 18549 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng0 41875 |
| [BourbakiEns] p. | Proposition 8 | fcof1 6542 fcofo 6543 |
| [BourbakiTop1] p. | Remark | xnegmnf 12041 xnegpnf 12040 |
| [BourbakiTop1] p. | Remark | rexneg 12042 |
| [BourbakiTop1] p. | Theorem | neiss 20913 |
| [BourbakiTop1] p. | Remark 3 | ust0 22023 ustfilxp 22016 |
| [BourbakiTop1] p. | Axiom GT' | tgpsubcn 21894 |
| [BourbakiTop1] p. | Example 1 | cstucnd 22088 iducn 22087 snfil 21668 |
| [BourbakiTop1] p. | Example 2 | neifil 21684 |
| [BourbakiTop1] p. | Theorem 1 | cnextcn 21871 |
| [BourbakiTop1] p. | Theorem 2 | ucnextcn 22108 |
| [BourbakiTop1] p. | Theorem 3 | df-hcmp 30003 |
| [BourbakiTop1] p. | Definition | istgp 21881 |
| [BourbakiTop1] p. | Paragraph 3 | infil 21667 |
| [BourbakiTop1] p. | Proposition | cnpco 21071 ishmeo 21562 neips 20917 |
| [BourbakiTop1] p. | Definition 1 | df-ucn 22080 df-ust 22004 filintn0 21665 ucnprima 22086 |
| [BourbakiTop1] p. | Definition 2 | df-cfilu 22091 |
| [BourbakiTop1] p. | Definition 3 | df-cusp 22102 df-usp 22061 df-utop 22035 trust 22033 |
| [BourbakiTop1] p. | Definition 6 | df-pcmp 29923 |
| [BourbakiTop1] p. | Condition F_I | ustssel 22009 |
| [BourbakiTop1] p. | Condition U_I | ustdiag 22012 |
| [BourbakiTop1] p. | Property V_iv | neiptopreu 20937 |
| [BourbakiTop1] p. | Proposition 1 | ucncn 22089 ustund 22025 ustuqtop 22050 |
| [BourbakiTop1] p. | Proposition 2 | neiptopreu 20937 utop2nei 22054 utop3cls 22055 |
| [BourbakiTop1] p. | Proposition 3 | fmucnd 22096 uspreg 22078 utopreg 22056 |
| [BourbakiTop1] p. | Proposition 4 | imasncld 21494 imasncls 21495 imasnopn 21493 |
| [BourbakiTop1] p. | Proposition 9 | cnpflf2 21804 |
| [BourbakiTop1] p. | Theorem 1 (d) | iscncl 21073 |
| [BourbakiTop1] p. | Condition F_II | ustincl 22011 |
| [BourbakiTop1] p. | Condition U_II | ustinvel 22013 |
| [BourbakiTop1] p. | Proposition 11 | cnextucn 22107 |
| [BourbakiTop1] p. | Proposition Vi | ssnei2 20920 |
| [BourbakiTop1] p. | Condition F_IIb | ustbasel 22010 |
| [BourbakiTop1] p. | Condition U_III | ustexhalf 22014 |
| [BourbakiTop1] p. | Definition C''' | df-cmp 21190 |
| [BourbakiTop1] p. | Proposition Vii | innei 20929 |
| [BourbakiTop1] p. | Proposition Viv | neissex 20931 |
| [BourbakiTop1] p. | Proposition Viii | elnei 20915 ssnei 20914 |
| [BourbakiTop1] p. | Remark below def. 1 | filn0 21666 |
| [BourbakiTop1] p. | Axioms FI, FIIa, FIIb, FIII) | df-fil 21650 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 20699 |
| [BourbakiTop2] p. 195 | Definition 1 | df-ldlf 29920 |
| [BrosowskiDeutsh] p. 89 | Proof follows | stoweidlem62 40279 |
| [BrosowskiDeutsh] p. 89 | Lemmas are written following | stowei 40281 stoweid 40280 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem1 40218 stoweidlem10 40227 stoweidlem14 40231 stoweidlem15 40232 stoweidlem35 40252 stoweidlem36 40253 stoweidlem37 40254 stoweidlem38 40255 stoweidlem40 40257 stoweidlem41 40258 stoweidlem43 40260 stoweidlem44 40261 stoweidlem46 40263 stoweidlem5 40222 stoweidlem50 40267 stoweidlem52 40269 stoweidlem53 40270 stoweidlem55 40272 stoweidlem56 40273 |
| [BrosowskiDeutsh] p. 90 | Lemma 1 | stoweidlem23 40240 stoweidlem24 40241 stoweidlem27 40244 stoweidlem28 40245 stoweidlem30 40247 |
| [BrosowskiDeutsh] p. 91 | Proof | stoweidlem34 40251 stoweidlem59 40276 stoweidlem60 40277 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem45 40262 stoweidlem49 40266 stoweidlem7 40224 |
| [BrosowskiDeutsh] p. 91 | Lemma 2 | stoweidlem31 40248 stoweidlem39 40256 stoweidlem42 40259 stoweidlem48 40265 stoweidlem51 40268 stoweidlem54 40271 stoweidlem57 40274 stoweidlem58 40275 |
| [BrosowskiDeutsh] p. 91 | Lemma 1 | stoweidlem25 40242 |
| [BrosowskiDeutsh] p. 91 | Lemma proves that the function ` ` (as defined | stoweidlem17 40234 |
| [BrosowskiDeutsh] p. 92 | Proof | stoweidlem11 40228 stoweidlem13 40230 stoweidlem26 40243 stoweidlem61 40278 |
| [BrosowskiDeutsh] p. 92 | Lemma 2 | stoweidlem18 40235 |
| [Bruck] p. 1 | Section I.1 | df-clintop 41836 df-mgm 17242 df-mgm2 41855 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 17284 df-sgrp2 41857 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3 17514 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4730 |
| [Church] p. 129 | Section II.24 | df-ifp 1013 dfifp2 1014 |
| [Clemente] p. 10 | Definition IT | natded 27260 |
| [Clemente] p. 10 | Definition I` `m,n | natded 27260 |
| [Clemente] p. 11 | Definition E=>m,n | natded 27260 |
| [Clemente] p. 11 | Definition I=>m,n | natded 27260 |
| [Clemente] p. 11 | Definition E` `(1) | natded 27260 |
| [Clemente] p. 11 | Definition E` `(2) | natded 27260 |
| [Clemente] p. 12 | Definition E` `m,n,p | natded 27260 |
| [Clemente] p. 12 | Definition I` `n(1) | natded 27260 |
| [Clemente] p. 12 | Definition I` `n(2) | natded 27260 |
| [Clemente] p. 13 | Definition I` `m,n,p | natded 27260 |
| [Clemente] p. 14 | Proof 5.11 | natded 27260 |
| [Clemente] p. 14 | Definition E` `n | natded 27260 |
| [Clemente] p. 15 | Theorem 5.2 | ex-natded5.2-2 27262 ex-natded5.2 27261 |
| [Clemente] p. 16 | Theorem 5.3 | ex-natded5.3-2 27265 ex-natded5.3 27264 |
| [Clemente] p. 18 | Theorem 5.5 | ex-natded5.5 27267 |
| [Clemente] p. 19 | Theorem 5.7 | ex-natded5.7-2 27269 ex-natded5.7 27268 |
| [Clemente] p. 20 | Theorem 5.8 | ex-natded5.8-2 27271 ex-natded5.8 27270 |
| [Clemente] p. 20 | Theorem 5.13 | ex-natded5.13-2 27273 ex-natded5.13 27272 |
| [Clemente] p. 32 | Definition I` `n | natded 27260 |
| [Clemente] p. 32 | Definition E` `m,n,p,a | natded 27260 |
| [Clemente] p. 32 | Definition E` `n,t | natded 27260 |
| [Clemente] p. 32 | Definition I` `n,t | natded 27260 |
| [Clemente] p. 43 | Theorem 9.20 | ex-natded9.20 27274 |
| [Clemente] p. 45 | Theorem 9.20 | ex-natded9.20-2 27275 |
| [Clemente] p. 45 | Theorem 9.26 | ex-natded9.26-2 27277 ex-natded9.26 27276 |
| [Cohen] p. 301 | Remark | relogoprlem 24337 |
| [Cohen] p. 301 | Property 2 | relogmul 24338 relogmuld 24371 |
| [Cohen] p. 301 | Property 3 | relogdiv 24339 relogdivd 24372 |
| [Cohen] p. 301 | Property 4 | relogexp 24342 |
| [Cohen] p. 301 | Property 1a | log1 24332 |
| [Cohen] p. 301 | Property 1b | loge 24333 |
| [Cohen4] p. 348 | Observation | relogbcxpb 24525 |
| [Cohen4] p. 349 | Property | relogbf 24529 |
| [Cohen4] p. 352 | Definition | elogb 24508 |
| [Cohen4] p. 361 | Property 2 | relogbmul 24515 |
| [Cohen4] p. 361 | Property 3 | logbrec 24520 relogbdiv 24517 |
| [Cohen4] p. 361 | Property 4 | relogbreexp 24513 |
| [Cohen4] p. 361 | Property 6 | relogbexp 24518 |
| [Cohen4] p. 361 | Property 1(a) | logbid1 24506 |
| [Cohen4] p. 361 | Property 1(b) | logb1 24507 |
| [Cohen4] p. 367 | Property | logbchbase 24509 |
| [Cohen4] p. 377 | Property 2 | logblt 24522 |
| [Cohn] p. 4 | Proposition 1.1.5 | sxbrsigalem1 30347 sxbrsigalem4 30349 |
| [Cohn] p. 81 | Section II.5 | acsdomd 17181 acsinfd 17180 acsinfdimd 17182 acsmap2d 17179 acsmapd 17178 |
| [Cohn] p. 143 | Example 5.1.1 | sxbrsiga 30352 |
| [Connell] p. 57 | Definition | df-scmat 20297 df-scmatalt 42188 |
| [CormenLeisersonRivest] p. 33 | Equation 2.4 | fldiv2 12660 |
| [Crawley] p. 1 | Definition of poset | df-poset 16946 |
| [Crawley] p. 107 | Theorem 13.2 | hlsupr 34672 |
| [Crawley] p. 110 | Theorem 13.3 | arglem1N 35477 dalaw 35172 |
| [Crawley] p. 111 | Theorem 13.4 | hlathil 37253 |
| [Crawley] p. 111 | Definition of set W | df-watsN 35276 |
| [Crawley] p. 111 | Definition of dilation | df-dilN 35392 df-ldil 35390 isldil 35396 |
| [Crawley] p. 111 | Definition of translation | df-ltrn 35391 df-trnN 35393 isltrn 35405 ltrnu 35407 |
| [Crawley] p. 112 | Lemma A | cdlema1N 35077 cdlema2N 35078 exatleN 34690 |
| [Crawley] p. 112 | Lemma B | 1cvrat 34762 cdlemb 35080 cdlemb2 35327 cdlemb3 35894 idltrn 35436 l1cvat 34342 lhpat 35329 lhpat2 35331 lshpat 34343 ltrnel 35425 ltrnmw 35437 |
| [Crawley] p. 112 | Lemma C | cdlemc1 35478 cdlemc2 35479 ltrnnidn 35461 trlat 35456 trljat1 35453 trljat2 35454 trljat3 35455 trlne 35472 trlnidat 35460 trlnle 35473 |
| [Crawley] p. 112 | Definition of automorphism | df-pautN 35277 |
| [Crawley] p. 113 | Lemma C | cdlemc 35484 cdlemc3 35480 cdlemc4 35481 |
| [Crawley] p. 113 | Lemma D | cdlemd 35494 cdlemd1 35485 cdlemd2 35486 cdlemd3 35487 cdlemd4 35488 cdlemd5 35489 cdlemd6 35490 cdlemd7 35491 cdlemd8 35492 cdlemd9 35493 cdleme31sde 35673 cdleme31se 35670 cdleme31se2 35671 cdleme31snd 35674 cdleme32a 35729 cdleme32b 35730 cdleme32c 35731 cdleme32d 35732 cdleme32e 35733 cdleme32f 35734 cdleme32fva 35725 cdleme32fva1 35726 cdleme32fvcl 35728 cdleme32le 35735 cdleme48fv 35787 cdleme4gfv 35795 cdleme50eq 35829 cdleme50f 35830 cdleme50f1 35831 cdleme50f1o 35834 cdleme50laut 35835 cdleme50ldil 35836 cdleme50lebi 35828 cdleme50rn 35833 cdleme50rnlem 35832 cdlemeg49le 35799 cdlemeg49lebilem 35827 |
| [Crawley] p. 113 | Lemma E | cdleme 35848 cdleme00a 35496 cdleme01N 35508 cdleme02N 35509 cdleme0a 35498 cdleme0aa 35497 cdleme0b 35499 cdleme0c 35500 cdleme0cp 35501 cdleme0cq 35502 cdleme0dN 35503 cdleme0e 35504 cdleme0ex1N 35510 cdleme0ex2N 35511 cdleme0fN 35505 cdleme0gN 35506 cdleme0moN 35512 cdleme1 35514 cdleme10 35541 cdleme10tN 35545 cdleme11 35557 cdleme11a 35547 cdleme11c 35548 cdleme11dN 35549 cdleme11e 35550 cdleme11fN 35551 cdleme11g 35552 cdleme11h 35553 cdleme11j 35554 cdleme11k 35555 cdleme11l 35556 cdleme12 35558 cdleme13 35559 cdleme14 35560 cdleme15 35565 cdleme15a 35561 cdleme15b 35562 cdleme15c 35563 cdleme15d 35564 cdleme16 35572 cdleme16aN 35546 cdleme16b 35566 cdleme16c 35567 cdleme16d 35568 cdleme16e 35569 cdleme16f 35570 cdleme16g 35571 cdleme19a 35591 cdleme19b 35592 cdleme19c 35593 cdleme19d 35594 cdleme19e 35595 cdleme19f 35596 cdleme1b 35513 cdleme2 35515 cdleme20aN 35597 cdleme20bN 35598 cdleme20c 35599 cdleme20d 35600 cdleme20e 35601 cdleme20f 35602 cdleme20g 35603 cdleme20h 35604 cdleme20i 35605 cdleme20j 35606 cdleme20k 35607 cdleme20l 35610 cdleme20l1 35608 cdleme20l2 35609 cdleme20m 35611 cdleme20y 35589 cdleme20zN 35588 cdleme21 35625 cdleme21d 35618 cdleme21e 35619 cdleme22a 35628 cdleme22aa 35627 cdleme22b 35629 cdleme22cN 35630 cdleme22d 35631 cdleme22e 35632 cdleme22eALTN 35633 cdleme22f 35634 cdleme22f2 35635 cdleme22g 35636 cdleme23a 35637 cdleme23b 35638 cdleme23c 35639 cdleme26e 35647 cdleme26eALTN 35649 cdleme26ee 35648 cdleme26f 35651 cdleme26f2 35653 cdleme26f2ALTN 35652 cdleme26fALTN 35650 cdleme27N 35657 cdleme27a 35655 cdleme27cl 35654 cdleme28c 35660 cdleme3 35524 cdleme30a 35666 cdleme31fv 35678 cdleme31fv1 35679 cdleme31fv1s 35680 cdleme31fv2 35681 cdleme31id 35682 cdleme31sc 35672 cdleme31sdnN 35675 cdleme31sn 35668 cdleme31sn1 35669 cdleme31sn1c 35676 cdleme31sn2 35677 cdleme31so 35667 cdleme35a 35736 cdleme35b 35738 cdleme35c 35739 cdleme35d 35740 cdleme35e 35741 cdleme35f 35742 cdleme35fnpq 35737 cdleme35g 35743 cdleme35h 35744 cdleme35h2 35745 cdleme35sn2aw 35746 cdleme35sn3a 35747 cdleme36a 35748 cdleme36m 35749 cdleme37m 35750 cdleme38m 35751 cdleme38n 35752 cdleme39a 35753 cdleme39n 35754 cdleme3b 35516 cdleme3c 35517 cdleme3d 35518 cdleme3e 35519 cdleme3fN 35520 cdleme3fa 35523 cdleme3g 35521 cdleme3h 35522 cdleme4 35525 cdleme40m 35755 cdleme40n 35756 cdleme40v 35757 cdleme40w 35758 cdleme41fva11 35765 cdleme41sn3aw 35762 cdleme41sn4aw 35763 cdleme41snaw 35764 cdleme42a 35759 cdleme42b 35766 cdleme42c 35760 cdleme42d 35761 cdleme42e 35767 cdleme42f 35768 cdleme42g 35769 cdleme42h 35770 cdleme42i 35771 cdleme42k 35772 cdleme42ke 35773 cdleme42keg 35774 cdleme42mN 35775 cdleme42mgN 35776 cdleme43aN 35777 cdleme43bN 35778 cdleme43cN 35779 cdleme43dN 35780 cdleme5 35527 cdleme50ex 35847 cdleme50ltrn 35845 cdleme51finvN 35844 cdleme51finvfvN 35843 cdleme51finvtrN 35846 cdleme6 35528 cdleme7 35536 cdleme7a 35530 cdleme7aa 35529 cdleme7b 35531 cdleme7c 35532 cdleme7d 35533 cdleme7e 35534 cdleme7ga 35535 cdleme8 35537 cdleme8tN 35542 cdleme9 35540 cdleme9a 35538 cdleme9b 35539 cdleme9tN 35544 cdleme9taN 35543 cdlemeda 35585 cdlemedb 35584 cdlemednpq 35586 cdlemednuN 35587 cdlemefr27cl 35691 cdlemefr32fva1 35698 cdlemefr32fvaN 35697 cdlemefrs32fva 35688 cdlemefrs32fva1 35689 cdlemefs27cl 35701 cdlemefs32fva1 35711 cdlemefs32fvaN 35710 cdlemesner 35583 cdlemeulpq 35507 |
| [Crawley] p. 114 | Lemma E | 4atex 35362 4atexlem7 35361 cdleme0nex 35577 cdleme17a 35573 cdleme17c 35575 cdleme17d 35786 cdleme17d1 35576 cdleme17d2 35783 cdleme18a 35578 cdleme18b 35579 cdleme18c 35580 cdleme18d 35582 cdleme4a 35526 |
| [Crawley] p. 115 | Lemma E | cdleme21a 35613 cdleme21at 35616 cdleme21b 35614 cdleme21c 35615 cdleme21ct 35617 cdleme21f 35620 cdleme21g 35621 cdleme21h 35622 cdleme21i 35623 cdleme22gb 35581 |
| [Crawley] p. 116 | Lemma F | cdlemf 35851 cdlemf1 35849 cdlemf2 35850 |
| [Crawley] p. 116 | Lemma G | cdlemftr1 35855 cdlemg16 35945 cdlemg28 35992 cdlemg28a 35981 cdlemg28b 35991 cdlemg3a 35885 cdlemg42 36017 cdlemg43 36018 cdlemg44 36021 cdlemg44a 36019 cdlemg46 36023 cdlemg47 36024 cdlemg9 35922 ltrnco 36007 ltrncom 36026 tgrpabl 36039 trlco 36015 |
| [Crawley] p. 116 | Definition of G | df-tgrp 36031 |
| [Crawley] p. 117 | Lemma G | cdlemg17 35965 cdlemg17b 35950 |
| [Crawley] p. 117 | Definition of E | df-edring-rN 36044 df-edring 36045 |
| [Crawley] p. 117 | Definition of trace-preserving endomorphism | istendo 36048 |
| [Crawley] p. 118 | Remark | tendopltp 36068 |
| [Crawley] p. 118 | Lemma H | cdlemh 36105 cdlemh1 36103 cdlemh2 36104 |
| [Crawley] p. 118 | Lemma I | cdlemi 36108 cdlemi1 36106 cdlemi2 36107 |
| [Crawley] p. 118 | Lemma J | cdlemj1 36109 cdlemj2 36110 cdlemj3 36111 tendocan 36112 |
| [Crawley] p. 118 | Lemma K | cdlemk 36262 cdlemk1 36119 cdlemk10 36131 cdlemk11 36137 cdlemk11t 36234 cdlemk11ta 36217 cdlemk11tb 36219 cdlemk11tc 36233 cdlemk11u-2N 36177 cdlemk11u 36159 cdlemk12 36138 cdlemk12u-2N 36178 cdlemk12u 36160 cdlemk13-2N 36164 cdlemk13 36140 cdlemk14-2N 36166 cdlemk14 36142 cdlemk15-2N 36167 cdlemk15 36143 cdlemk16-2N 36168 cdlemk16 36145 cdlemk16a 36144 cdlemk17-2N 36169 cdlemk17 36146 cdlemk18-2N 36174 cdlemk18-3N 36188 cdlemk18 36156 cdlemk19-2N 36175 cdlemk19 36157 cdlemk19u 36258 cdlemk1u 36147 cdlemk2 36120 cdlemk20-2N 36180 cdlemk20 36162 cdlemk21-2N 36179 cdlemk21N 36161 cdlemk22-3 36189 cdlemk22 36181 cdlemk23-3 36190 cdlemk24-3 36191 cdlemk25-3 36192 cdlemk26-3 36194 cdlemk26b-3 36193 cdlemk27-3 36195 cdlemk28-3 36196 cdlemk29-3 36199 cdlemk3 36121 cdlemk30 36182 cdlemk31 36184 cdlemk32 36185 cdlemk33N 36197 cdlemk34 36198 cdlemk35 36200 cdlemk36 36201 cdlemk37 36202 cdlemk38 36203 cdlemk39 36204 cdlemk39u 36256 cdlemk4 36122 cdlemk41 36208 cdlemk42 36229 cdlemk42yN 36232 cdlemk43N 36251 cdlemk45 36235 cdlemk46 36236 cdlemk47 36237 cdlemk48 36238 cdlemk49 36239 cdlemk5 36124 cdlemk50 36240 cdlemk51 36241 cdlemk52 36242 cdlemk53 36245 cdlemk54 36246 cdlemk55 36249 cdlemk55u 36254 cdlemk56 36259 cdlemk5a 36123 cdlemk5auN 36148 cdlemk5u 36149 cdlemk6 36125 cdlemk6u 36150 cdlemk7 36136 cdlemk7u-2N 36176 cdlemk7u 36158 cdlemk8 36126 cdlemk9 36127 cdlemk9bN 36128 cdlemki 36129 cdlemkid 36224 cdlemkj-2N 36170 cdlemkj 36151 cdlemksat 36134 cdlemksel 36133 cdlemksv 36132 cdlemksv2 36135 cdlemkuat 36154 cdlemkuel-2N 36172 cdlemkuel-3 36186 cdlemkuel 36153 cdlemkuv-2N 36171 cdlemkuv2-2 36173 cdlemkuv2-3N 36187 cdlemkuv2 36155 cdlemkuvN 36152 cdlemkvcl 36130 cdlemky 36214 cdlemkyyN 36250 tendoex 36263 |
| [Crawley] p. 120 | Remark | dva1dim 36273 |
| [Crawley] p. 120 | Lemma L | cdleml1N 36264 cdleml2N 36265 cdleml3N 36266 cdleml4N 36267 cdleml5N 36268 cdleml6 36269 cdleml7 36270 cdleml8 36271 cdleml9 36272 dia1dim 36350 |
| [Crawley] p. 120 | Lemma M | dia11N 36337 diaf11N 36338 dialss 36335 diaord 36336 dibf11N 36450 djajN 36426 |
| [Crawley] p. 120 | Definition of isomorphism map | diaval 36321 |
| [Crawley] p. 121 | Lemma M | cdlemm10N 36407 dia2dimlem1 36353 dia2dimlem2 36354 dia2dimlem3 36355 dia2dimlem4 36356 dia2dimlem5 36357 diaf1oN 36419 diarnN 36418 dvheveccl 36401 dvhopN 36405 |
| [Crawley] p. 121 | Lemma N | cdlemn 36501 cdlemn10 36495 cdlemn11 36500 cdlemn11a 36496 cdlemn11b 36497 cdlemn11c 36498 cdlemn11pre 36499 cdlemn2 36484 cdlemn2a 36485 cdlemn3 36486 cdlemn4 36487 cdlemn4a 36488 cdlemn5 36490 cdlemn5pre 36489 cdlemn6 36491 cdlemn7 36492 cdlemn8 36493 cdlemn9 36494 diclspsn 36483 |
| [Crawley] p. 121 | Definition of phi(q) | df-dic 36462 |
| [Crawley] p. 122 | Lemma N | dih11 36554 dihf11 36556 dihjust 36506 dihjustlem 36505 dihord 36553 dihord1 36507 dihord10 36512 dihord11b 36511 dihord11c 36513 dihord2 36516 dihord2a 36508 dihord2b 36509 dihord2cN 36510 dihord2pre 36514 dihord2pre2 36515 dihordlem6 36502 dihordlem7 36503 dihordlem7b 36504 |
| [Crawley] p. 122 | Definition of isomorphism map | dihffval 36519 dihfval 36520 dihval 36521 |
| [Diestel] p. 3 | Section 1.1 | df-cusgr 26232 df-nbgr 26228 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 26160 uhgrspan1 26195 uhgrspansubgr 26183 |
| [Diestel] p. 5 | Proposition 1.2.1 | fusgrvtxdgonume 26450 vtxdgoddnumeven 26449 |
| [Diestel] p. 27 | Section 1.10 | df-ushgr 25954 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3577 |
| [Eisenberg] p. 82 | Definition 6.3 | dfom3 8544 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 7859 |
| [Eisenberg] p. 216 | Example 13.2(4) | omenps 8552 |
| [Eisenberg] p. 310 | Theorem 19.8 | cardprc 8806 |
| [Eisenberg] p. 310 | Corollary 19.7(2) | cardsdom 9377 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4788 |
| [Enderton] p. 19 | Definition | df-tp 4182 |
| [Enderton] p. 26 | Exercise 5 | unissb 4469 |
| [Enderton] p. 26 | Exercise 10 | pwel 4920 |
| [Enderton] p. 28 | Exercise 7(b) | pwun 5022 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1 4591 iinin2 4590 iinun2 4586 iunin1 4585 iunin1f 29374 iunin2 4584 uniin1 29367 uniin2 29368 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2 4589 iundif2 4587 |
| [Enderton] p. 32 | Exercise 20 | unineq 3877 |
| [Enderton] p. 33 | Exercise 23 | iinuni 4609 |
| [Enderton] p. 33 | Exercise 25 | iununi 4610 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4617 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 6978 iunpwss 4618 |
| [Enderton] p. 36 | Definition | opthwiener 4976 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4918 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4474 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4939 rnex 7100 rnexg 7098 |
| [Enderton] p. 41 | Exercise 8 | dmuni 5334 rnuni 5544 |
| [Enderton] p. 42 | Definition of a function | dffun7 5915 dffun8 5916 |
| [Enderton] p. 43 | Definition of function value | funfv2 6266 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5958 |
| [Enderton] p. 44 | Definition (d) | dfima2 5468 dfima3 5469 |
| [Enderton] p. 47 | Theorem 3H | fvco2 6273 |
| [Enderton] p. 49 | Axiom of Choice (first form) | ac7 9295 ac7g 9296 df-ac 8939 dfac2 8953 dfac2a 8952 dfac3 8944 dfac7 8954 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 6504 |
| [Enderton] p. 52 | Definition | df-map 7859 |
| [Enderton] p. 53 | Exercise 21 | coass 5654 |
| [Enderton] p. 53 | Exercise 27 | dmco 5643 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5965 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5501 |
| [Enderton] p. 54 | Remark | ixpf 7930 ixpssmap 7942 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 7909 |
| [Enderton] p. 55 | Axiom of Choice (second form) | ac9 9305 ac9s 9315 |
| [Enderton] p. 56 | Theorem 3M | erref 7762 |
| [Enderton] p. 57 | Lemma 3N | erthi 7793 |
| [Enderton] p. 57 | Definition | df-ec 7744 |
| [Enderton] p. 58 | Definition | df-qs 7748 |
| [Enderton] p. 61 | Exercise 35 | df-ec 7744 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 5331 |
| [Enderton] p. 68 | Definition of successor | df-suc 5729 |
| [Enderton] p. 71 | Definition | df-tr 4753 dftr4 4757 |
| [Enderton] p. 72 | Theorem 4E | unisuc 5801 |
| [Enderton] p. 73 | Exercise 6 | unisuc 5801 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4767 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4768 trintALT 39117 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 7684 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 7686 onasuc 7608 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6653 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 7685 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 7687 onmsuc 7609 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 7702 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 7689 nnacom 7697 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 7703 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 7704 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 7706 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 7690 nnmsucr 7705 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 7718 |
| [Enderton] p. 129 | Definition | df-en 7956 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 6608 |
| [Enderton] p. 133 | Exercise 1 | xpomen 8838 |
| [Enderton] p. 133 | Exercise 2 | qnnen 14942 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | php 8144 |
| [Enderton] p. 135 | Corollary 6C | php3 8146 |
| [Enderton] p. 136 | Corollary 6E | nneneq 8143 |
| [Enderton] p. 136 | Corollary 6D(a) | pssinf 8170 |
| [Enderton] p. 136 | Corollary 6D(b) | ominf 8172 |
| [Enderton] p. 137 | Lemma 6F | pssnn 8178 |
| [Enderton] p. 138 | Corollary 6G | ssfi 8180 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 8124 |
| [Enderton] p. 142 | Theorem 6I(3) | xpcdaen 9005 |
| [Enderton] p. 142 | Theorem 6I(4) | mapcdaen 9006 |
| [Enderton] p. 143 | Theorem 6J | cda0en 9001 cda1en 8997 |
| [Enderton] p. 144 | Exercise 13 | iunfi 8254 unifi 8255 unifi2 8256 |
| [Enderton] p. 144 | Corollary 6K | undif2 4044 unfi 8227 unfi2 8229 |
| [Enderton] p. 145 | Figure 38 | ffoss 7127 |
| [Enderton] p. 145 | Definition | df-dom 7957 |
| [Enderton] p. 146 | Example 1 | domen 7968 domeng 7969 |
| [Enderton] p. 146 | Example 3 | nndomo 8154 nnsdom 8551 nnsdomg 8219 |
| [Enderton] p. 149 | Theorem 6L(a) | cdadom2 9009 |
| [Enderton] p. 149 | Theorem 6L(c) | mapdom1 8125 xpdom1 8059 xpdom1g 8057 xpdom2g 8056 |
| [Enderton] p. 149 | Theorem 6L(d) | mapdom2 8131 |
| [Enderton] p. 151 | Theorem 6M | zorn 9329 zorng 9326 |
| [Enderton] p. 151 | Theorem 6M(4) | ac8 9314 dfac5 8951 |
| [Enderton] p. 159 | Theorem 6Q | unictb 9397 |
| [Enderton] p. 164 | Example | infdif 9031 |
| [Enderton] p. 168 | Definition | df-po 5035 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 5835 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 5771 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 5834 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 5778 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 7038 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 6987 |
| [Enderton] p. 194 | Remark | onprc 6984 |
| [Enderton] p. 194 | Exercise 16 | suc11 5831 |
| [Enderton] p. 197 | Definition | df-card 8765 |
| [Enderton] p. 197 | Theorem 7P | carden 9373 |
| [Enderton] p. 200 | Exercise 25 | tfis 7054 |
| [Enderton] p. 202 | Lemma 7T | r1tr 8639 |
| [Enderton] p. 202 | Definition | df-r1 8627 |
| [Enderton] p. 202 | Theorem 7Q | r1val1 8649 |
| [Enderton] p. 204 | Theorem 7V(b) | rankval4 8730 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 8510 |
| [Enderton] p. 207 | Exercise 30 | rankpr 8720 rankprb 8714 rankpw 8706 rankpwi 8686 rankuniss 8729 |
| [Enderton] p. 207 | Exercise 34 | opthreg 8515 |
| [Enderton] p. 208 | Exercise 35 | suc11reg 8516 |
| [Enderton] p. 212 | Definition of aleph | alephval3 8933 |
| [Enderton] p. 213 | Theorem 8A(a) | alephord2 8899 |
| [Enderton] p. 213 | Theorem 8A(b) | cardalephex 8913 |
| [Enderton] p. 218 | Theorem Schema 8E | onfununi 7438 |
| [Enderton] p. 222 | Definition of kard | karden 8758 kardex 8757 |
| [Enderton] p. 238 | Theorem 8R | oeoa 7677 |
| [Enderton] p. 238 | Theorem 8S | oeoe 7679 |
| [Enderton] p. 240 | Exercise 25 | oarec 7642 |
| [Enderton] p. 257 | Definition of cofinality | cflm 9072 |
| [FaureFrolicher] p. 57 | Definition 3.1.9 | mreexd 16302 |
| [FaureFrolicher] p. 83 | Definition 4.1.1 | df-mri 16248 |
| [FaureFrolicher] p. 83 | Proposition 4.1.3 | acsfiindd 17177 mrieqv2d 16299 mrieqvd 16298 |
| [FaureFrolicher] p. 84 | Lemma 4.1.5 | mreexmrid 16303 |
| [FaureFrolicher] p. 86 | Proposition 4.2.1 | mreexexd 16308 mreexexlem2d 16305 |
| [FaureFrolicher] p. 87 | Theorem 4.2.2 | acsexdimd 17183 mreexfidimd 16311 |
| [Frege1879] p. 11 | Statement | df3or2 38060 |
| [Frege1879] p. 12 | Statement | df3an2 38061 dfxor4 38058 dfxor5 38059 |
| [Frege1879] p. 26 | Axiom 1 | ax-frege1 38084 |
| [Frege1879] p. 26 | Axiom 2 | ax-frege2 38085 |
| [Frege1879] p. 26 | Proposition 1 | ax-1 6 |
| [Frege1879] p. 26 | Proposition 2 | ax-2 7 |
| [Frege1879] p. 29 | Proposition 3 | frege3 38089 |
| [Frege1879] p. 31 | Proposition 4 | frege4 38093 |
| [Frege1879] p. 32 | Proposition 5 | frege5 38094 |
| [Frege1879] p. 33 | Proposition 6 | frege6 38100 |
| [Frege1879] p. 34 | Proposition 7 | frege7 38102 |
| [Frege1879] p. 35 | Axiom 8 | ax-frege8 38103 axfrege8 38101 |
| [Frege1879] p. 35 | Proposition 8 | pm2.04 90 wl-pm2.04 33267 |
| [Frege1879] p. 35 | Proposition 9 | frege9 38106 |
| [Frege1879] p. 36 | Proposition 10 | frege10 38114 |
| [Frege1879] p. 36 | Proposition 11 | frege11 38108 |
| [Frege1879] p. 37 | Proposition 12 | frege12 38107 |
| [Frege1879] p. 37 | Proposition 13 | frege13 38116 |
| [Frege1879] p. 37 | Proposition 14 | frege14 38117 |
| [Frege1879] p. 38 | Proposition 15 | frege15 38120 |
| [Frege1879] p. 38 | Proposition 16 | frege16 38110 |
| [Frege1879] p. 39 | Proposition 17 | frege17 38115 |
| [Frege1879] p. 39 | Proposition 18 | frege18 38112 |
| [Frege1879] p. 39 | Proposition 19 | frege19 38118 |
| [Frege1879] p. 40 | Proposition 20 | frege20 38122 |
| [Frege1879] p. 40 | Proposition 21 | frege21 38121 |
| [Frege1879] p. 41 | Proposition 22 | frege22 38113 |
| [Frege1879] p. 42 | Proposition 23 | frege23 38119 |
| [Frege1879] p. 42 | Proposition 24 | frege24 38109 |
| [Frege1879] p. 42 | Proposition 25 | frege25 38111 rp-frege25 38099 |
| [Frege1879] p. 42 | Proposition 26 | frege26 38104 |
| [Frege1879] p. 43 | Axiom 28 | ax-frege28 38124 |
| [Frege1879] p. 43 | Proposition 27 | frege27 38105 |
| [Frege1879] p. 43 | Proposition 28 | con3 149 |
| [Frege1879] p. 43 | Proposition 29 | frege29 38125 |
| [Frege1879] p. 44 | Axiom 31 | ax-frege31 38128 axfrege31 38127 |
| [Frege1879] p. 44 | Proposition 30 | frege30 38126 |
| [Frege1879] p. 44 | Proposition 31 | notnotr 125 |
| [Frege1879] p. 44 | Proposition 32 | frege32 38129 |
| [Frege1879] p. 44 | Proposition 33 | frege33 38130 |
| [Frege1879] p. 45 | Proposition 34 | frege34 38131 |
| [Frege1879] p. 45 | Proposition 35 | frege35 38132 |
| [Frege1879] p. 45 | Proposition 36 | frege36 38133 |
| [Frege1879] p. 46 | Proposition 37 | frege37 38134 |
| [Frege1879] p. 46 | Proposition 38 | frege38 38135 |
| [Frege1879] p. 46 | Proposition 39 | frege39 38136 |
| [Frege1879] p. 46 | Proposition 40 | frege40 38137 |
| [Frege1879] p. 47 | Axiom 41 | ax-frege41 38139 axfrege41 38138 |
| [Frege1879] p. 47 | Proposition 41 | notnot 136 |
| [Frege1879] p. 47 | Proposition 42 | frege42 38140 |
| [Frege1879] p. 47 | Proposition 43 | frege43 38141 |
| [Frege1879] p. 47 | Proposition 44 | frege44 38142 |
| [Frege1879] p. 47 | Proposition 45 | frege45 38143 |
| [Frege1879] p. 48 | Proposition 46 | frege46 38144 |
| [Frege1879] p. 48 | Proposition 47 | frege47 38145 |
| [Frege1879] p. 49 | Proposition 48 | frege48 38146 |
| [Frege1879] p. 49 | Proposition 49 | frege49 38147 |
| [Frege1879] p. 49 | Proposition 50 | frege50 38148 |
| [Frege1879] p. 50 | Axiom 52 | ax-frege52a 38151 ax-frege52c 38182 frege52aid 38152 frege52b 38183 |
| [Frege1879] p. 50 | Axiom 54 | ax-frege54a 38156 ax-frege54c 38186 frege54b 38187 |
| [Frege1879] p. 50 | Proposition 51 | frege51 38149 |
| [Frege1879] p. 50 | Proposition 52 | dfsbcq 3437 |
| [Frege1879] p. 50 | Proposition 53 | frege53a 38154 frege53aid 38153 frege53b 38184 frege53c 38208 |
| [Frege1879] p. 50 | Proposition 54 | biid 251 eqid 2622 |
| [Frege1879] p. 50 | Proposition 55 | frege55a 38162 frege55aid 38159 frege55b 38191 frege55c 38212 frege55cor1a 38163 frege55lem2a 38161 frege55lem2b 38190 frege55lem2c 38211 |
| [Frege1879] p. 50 | Proposition 56 | frege56a 38165 frege56aid 38164 frege56b 38192 frege56c 38213 |
| [Frege1879] p. 51 | Axiom 58 | ax-frege58a 38169 ax-frege58b 38195 frege58bid 38196 frege58c 38215 |
| [Frege1879] p. 51 | Proposition 57 | frege57a 38167 frege57aid 38166 frege57b 38193 frege57c 38214 |
| [Frege1879] p. 51 | Proposition 58 | spsbc 3448 |
| [Frege1879] p. 51 | Proposition 59 | frege59a 38171 frege59b 38198 frege59c 38216 |
| [Frege1879] p. 52 | Proposition 60 | frege60a 38172 frege60b 38199 frege60c 38217 |
| [Frege1879] p. 52 | Proposition 61 | frege61a 38173 frege61b 38200 frege61c 38218 |
| [Frege1879] p. 52 | Proposition 62 | frege62a 38174 frege62b 38201 frege62c 38219 |
| [Frege1879] p. 52 | Proposition 63 | frege63a 38175 frege63b 38202 frege63c 38220 |
| [Frege1879] p. 53 | Proposition 64 | frege64a 38176 frege64b 38203 frege64c 38221 |
| [Frege1879] p. 53 | Proposition 65 | frege65a 38177 frege65b 38204 frege65c 38222 |
| [Frege1879] p. 54 | Proposition 66 | frege66a 38178 frege66b 38205 frege66c 38223 |
| [Frege1879] p. 54 | Proposition 67 | frege67a 38179 frege67b 38206 frege67c 38224 |
| [Frege1879] p. 54 | Proposition 68 | frege68a 38180 frege68b 38207 frege68c 38225 |
| [Frege1879] p. 55 | Definition 69 | dffrege69 38226 |
| [Frege1879] p. 58 | Proposition 70 | frege70 38227 |
| [Frege1879] p. 59 | Proposition 71 | frege71 38228 |
| [Frege1879] p. 59 | Proposition 72 | frege72 38229 |
| [Frege1879] p. 59 | Proposition 73 | frege73 38230 |
| [Frege1879] p. 60 | Definition 76 | dffrege76 38233 |
| [Frege1879] p. 60 | Proposition 74 | frege74 38231 |
| [Frege1879] p. 60 | Proposition 75 | frege75 38232 |
| [Frege1879] p. 62 | Proposition 77 | frege77 38234 frege77d 38038 |
| [Frege1879] p. 63 | Proposition 78 | frege78 38235 |
| [Frege1879] p. 63 | Proposition 79 | frege79 38236 |
| [Frege1879] p. 63 | Proposition 80 | frege80 38237 |
| [Frege1879] p. 63 | Proposition 81 | frege81 38238 frege81d 38039 |
| [Frege1879] p. 64 | Proposition 82 | frege82 38239 |
| [Frege1879] p. 65 | Proposition 83 | frege83 38240 frege83d 38040 |
| [Frege1879] p. 65 | Proposition 84 | frege84 38241 |
| [Frege1879] p. 66 | Proposition 85 | frege85 38242 |
| [Frege1879] p. 66 | Proposition 86 | frege86 38243 |
| [Frege1879] p. 66 | Proposition 87 | frege87 38244 frege87d 38042 |
| [Frege1879] p. 67 | Proposition 88 | frege88 38245 |
| [Frege1879] p. 68 | Proposition 89 | frege89 38246 |
| [Frege1879] p. 68 | Proposition 90 | frege90 38247 |
| [Frege1879] p. 68 | Proposition 91 | frege91 38248 frege91d 38043 |
| [Frege1879] p. 69 | Proposition 92 | frege92 38249 |
| [Frege1879] p. 70 | Proposition 93 | frege93 38250 |
| [Frege1879] p. 70 | Proposition 94 | frege94 38251 |
| [Frege1879] p. 70 | Proposition 95 | frege95 38252 |
| [Frege1879] p. 71 | Definition 99 | dffrege99 38256 |
| [Frege1879] p. 71 | Proposition 96 | frege96 38253 frege96d 38041 |
| [Frege1879] p. 71 | Proposition 97 | frege97 38254 frege97d 38044 |
| [Frege1879] p. 71 | Proposition 98 | frege98 38255 frege98d 38045 |
| [Frege1879] p. 72 | Proposition 100 | frege100 38257 |
| [Frege1879] p. 72 | Proposition 101 | frege101 38258 |
| [Frege1879] p. 72 | Proposition 102 | frege102 38259 frege102d 38046 |
| [Frege1879] p. 73 | Proposition 103 | frege103 38260 |
| [Frege1879] p. 73 | Proposition 104 | frege104 38261 |
| [Frege1879] p. 73 | Proposition 105 | frege105 38262 |
| [Frege1879] p. 73 | Proposition 106 | frege106 38263 frege106d 38047 |
| [Frege1879] p. 74 | Proposition 107 | frege107 38264 |
| [Frege1879] p. 74 | Proposition 108 | frege108 38265 frege108d 38048 |
| [Frege1879] p. 74 | Proposition 109 | frege109 38266 frege109d 38049 |
| [Frege1879] p. 75 | Proposition 110 | frege110 38267 |
| [Frege1879] p. 75 | Proposition 111 | frege111 38268 frege111d 38051 |
| [Frege1879] p. 76 | Proposition 112 | frege112 38269 |
| [Frege1879] p. 76 | Proposition 113 | frege113 38270 |
| [Frege1879] p. 76 | Proposition 114 | frege114 38271 frege114d 38050 |
| [Frege1879] p. 77 | Definition 115 | dffrege115 38272 |
| [Frege1879] p. 77 | Proposition 116 | frege116 38273 |
| [Frege1879] p. 78 | Proposition 117 | frege117 38274 |
| [Frege1879] p. 78 | Proposition 118 | frege118 38275 |
| [Frege1879] p. 78 | Proposition 119 | frege119 38276 |
| [Frege1879] p. 78 | Proposition 120 | frege120 38277 |
| [Frege1879] p. 79 | Proposition 121 | frege121 38278 |
| [Frege1879] p. 79 | Proposition 122 | frege122 38279 frege122d 38052 |
| [Frege1879] p. 79 | Proposition 123 | frege123 38280 |
| [Frege1879] p. 80 | Proposition 124 | frege124 38281 frege124d 38053 |
| [Frege1879] p. 81 | Proposition 125 | frege125 38282 |
| [Frege1879] p. 81 | Proposition 126 | frege126 38283 frege126d 38054 |
| [Frege1879] p. 82 | Proposition 127 | frege127 38284 |
| [Frege1879] p. 83 | Proposition 128 | frege128 38285 |
| [Frege1879] p. 83 | Proposition 129 | frege129 38286 frege129d 38055 |
| [Frege1879] p. 84 | Proposition 130 | frege130 38287 |
| [Frege1879] p. 85 | Proposition 131 | frege131 38288 frege131d 38056 |
| [Frege1879] p. 86 | Proposition 132 | frege132 38289 |
| [Frege1879] p. 86 | Proposition 133 | frege133 38290 frege133d 38057 |
| [Fremlin1] p. 13 | Definition 111G (b) | df-salgen 40533 |
| [Fremlin1] p. 13 | Definition 111G (d) | borelmbl 40850 |
| [Fremlin1] p. 13 | Proposition 111G (b) | salgenss 40554 |
| [Fremlin1] p. 14 | Definition 112A | ismea 40668 |
| [Fremlin1] p. 15 | Remark 112B (d) | psmeasure 40688 |
| [Fremlin1] p. 15 | Property 112C (a) | meadjun 40679 meadjunre 40693 |
| [Fremlin1] p. 15 | Property 112C (b) | meassle 40680 |
| [Fremlin1] p. 15 | Property 112C (c) | meaunle 40681 |
| [Fremlin1] p. 16 | Property 112C (d) | iundjiun 40677 meaiunle 40686 meaiunlelem 40685 |
| [Fremlin1] p. 16 | Proposition 112C (e) | meaiuninc 40698 meaiuninc2 40699 meaiuninclem 40697 |
| [Fremlin1] p. 16 | Proposition 112C (f) | meaiininc 40701 meaiininc2 40702 meaiininclem 40700 |
| [Fremlin1] p. 19 | Theorem 113C | caragen0 40720 caragendifcl 40728 caratheodory 40742 omelesplit 40732 |
| [Fremlin1] p. 19 | Definition 113A | isome 40708 isomennd 40745 isomenndlem 40744 |
| [Fremlin1] p. 19 | Remark 113B (c) | omeunle 40730 |
| [Fremlin1] p. 19 | Definition 112Df | caragencmpl 40749 voncmpl 40835 |
| [Fremlin1] p. 19 | Definition 113A (ii) | omessle 40712 |
| [Fremlin1] p. 20 | Theorem 113C | carageniuncl 40737 carageniuncllem1 40735 carageniuncllem2 40736 caragenuncl 40727 caragenuncllem 40726 caragenunicl 40738 |
| [Fremlin1] p. 21 | Remark 113D | caragenel2d 40746 |
| [Fremlin1] p. 21 | Theorem 113C | caratheodorylem1 40740 caratheodorylem2 40741 |
| [Fremlin1] p. 21 | Exercise 113Xa | caragencmpl 40749 |
| [Fremlin1] p. 23 | Lemma 114B | hoidmv1le 40808 hoidmv1lelem1 40805 hoidmv1lelem2 40806 hoidmv1lelem3 40807 |
| [Fremlin1] p. 25 | Definition 114E | isvonmbl 40852 |
| [Fremlin1] p. 29 | Lemma 115B | hoidmv1le 40808 hoidmvle 40814 hoidmvlelem1 40809 hoidmvlelem2 40810 hoidmvlelem3 40811 hoidmvlelem4 40812 hoidmvlelem5 40813 hsphoidmvle2 40799 hsphoif 40790 hsphoival 40793 |
| [Fremlin1] p. 29 | Definition 1135 (b) | hoicvr 40762 |
| [Fremlin1] p. 29 | Definition 115A (b) | hoicvrrex 40770 |
| [Fremlin1] p. 29 | Definition 115A (c) | hoidmv0val 40797 hoidmvn0val 40798 hoidmvval 40791 hoidmvval0 40801 hoidmvval0b 40804 |
| [Fremlin1] p. 30 | Lemma 115B | hoiprodp1 40802 hsphoidmvle 40800 |
| [Fremlin1] p. 30 | Definition 115C | df-ovoln 40751 df-voln 40753 |
| [Fremlin1] p. 30 | Proposition 115D (a) | dmovn 40818 ovn0 40780 ovn0lem 40779 ovnf 40777 ovnome 40787 ovnssle 40775 ovnsslelem 40774 ovnsupge0 40771 |
| [Fremlin1] p. 30 | Proposition 115D (b) | ovnhoi 40817 ovnhoilem1 40815 ovnhoilem2 40816 vonhoi 40881 |
| [Fremlin1] p. 31 | Lemma 115F | hoidifhspdmvle 40834 hoidifhspf 40832 hoidifhspval 40822 hoidifhspval2 40829 hoidifhspval3 40833 hspmbl 40843 hspmbllem1 40840 hspmbllem2 40841 hspmbllem3 40842 |
| [Fremlin1] p. 31 | Definition 115E | voncmpl 40835 vonmea 40788 |
| [Fremlin1] p. 31 | Proposition 115D (a)(iv) | ovnsubadd 40786 ovnsubadd2 40860 ovnsubadd2lem 40859 ovnsubaddlem1 40784 ovnsubaddlem2 40785 |
| [Fremlin1] p. 32 | Proposition 115G (a) | hoimbl 40845 hoimbl2 40879 hoimbllem 40844 hspdifhsp 40830 opnvonmbl 40848 opnvonmbllem2 40847 |
| [Fremlin1] p. 32 | Proposition 115G (b) | borelmbl 40850 |
| [Fremlin1] p. 32 | Proposition 115G (c) | iccvonmbl 40893 iccvonmbllem 40892 ioovonmbl 40891 |
| [Fremlin1] p. 32 | Proposition 115G (d) | vonicc 40899 vonicclem2 40898 vonioo 40896 vonioolem2 40895 vonn0icc 40902 vonn0icc2 40906 vonn0ioo 40901 vonn0ioo2 40904 |
| [Fremlin1] p. 32 | Proposition 115G (e) | ctvonmbl 40903 snvonmbl 40900 vonct 40907 vonsn 40905 |
| [Fremlin1] p. 35 | Lemma 121A | subsalsal 40577 |
| [Fremlin1] p. 35 | Lemma 121A (iii) | subsaliuncl 40576 subsaliuncllem 40575 |
| [Fremlin1] p. 35 | Proposition 121B | salpreimagtge 40934 salpreimalegt 40920 salpreimaltle 40935 |
| [Fremlin1] p. 35 | Proposition 121B (i) | issmf 40937 issmff 40943 issmflem 40936 |
| [Fremlin1] p. 35 | Proposition 121B (ii) | issmfle 40954 issmflelem 40953 smfpreimale 40963 |
| [Fremlin1] p. 35 | Proposition 121B (iii) | issmfgt 40965 issmfgtlem 40964 |
| [Fremlin1] p. 36 | Definition 121C | df-smblfn 40910 issmf 40937 issmff 40943 issmfge 40978 issmfgelem 40977 issmfgt 40965 issmfgtlem 40964 issmfle 40954 issmflelem 40953 issmflem 40936 |
| [Fremlin1] p. 36 | Proposition 121B | salpreimagelt 40918 salpreimagtlt 40939 salpreimalelt 40938 |
| [Fremlin1] p. 36 | Proposition 121B (iv) | issmfge 40978 issmfgelem 40977 |
| [Fremlin1] p. 36 | Proposition 121D (a) | bormflebmf 40962 |
| [Fremlin1] p. 36 | Proposition 121D (b) | cnfrrnsmf 40960 cnfsmf 40949 |
| [Fremlin1] p. 36 | Proposition 121D (c) | decsmf 40975 decsmflem 40974 incsmf 40951 incsmflem 40950 |
| [Fremlin1] p. 37 | Proposition 121E (a) | pimconstlt0 40914 pimconstlt1 40915 smfconst 40958 |
| [Fremlin1] p. 37 | Proposition 121E (b) | smfadd 40973 smfaddlem1 40971 smfaddlem2 40972 |
| [Fremlin1] p. 37 | Proposition 121E (c) | smfmulc1 41003 |
| [Fremlin1] p. 37 | Proposition 121E (d) | smfmul 41002 smfmullem1 40998 smfmullem2 40999 smfmullem3 41000 smfmullem4 41001 |
| [Fremlin1] p. 37 | Proposition 121E (e) | smfdiv 41004 |
| [Fremlin1] p. 37 | Proposition 121E (f) | smfpimbor1 41007 smfpimbor1lem2 41006 |
| [Fremlin1] p. 37 | Proposition 121E (g) | smfco 41009 |
| [Fremlin1] p. 37 | Proposition 121E (h) | smfres 40997 |
| [Fremlin1] p. 38 | Proposition 121E (e) | smfrec 40996 |
| [Fremlin1] p. 38 | Proposition 121E (f) | smfpimbor1lem1 41005 smfresal 40995 |
| [Fremlin1] p. 38 | Proposition 121F (a) | smflim 40985 smflim2 41012 smflimlem1 40979 smflimlem2 40980 smflimlem3 40981 smflimlem4 40982 smflimlem5 40983 smflimlem6 40984 smflimmpt 41016 |
| [Fremlin1] p. 38 | Proposition 121F (b) | smfsup 41020 smfsuplem1 41017 smfsuplem2 41018 smfsuplem3 41019 smfsupmpt 41021 smfsupxr 41022 |
| [Fremlin1] p. 38 | Proposition 121F (c) | smfinf 41024 smfinflem 41023 smfinfmpt 41025 |
| [Fremlin1] p. 39 | Remark 121G | smflim 40985 smflim2 41012 smflimmpt 41016 |
| [Fremlin1] p. 39 | Proposition 121F | smfpimcc 41014 |
| [Fremlin1] p. 39 | Proposition 121F (d) | smflimsup 41034 smflimsuplem2 41027 smflimsuplem6 41031 smflimsuplem7 41032 smflimsuplem8 41033 smflimsupmpt 41035 |
| [Fremlin1] p. 39 | Proposition 121F (e) | smfliminf 41037 smfliminflem 41036 smfliminfmpt 41038 |
| [Fremlin1] p. 80 | Definition 135E (b) | df-smblfn 40910 |
| [Fremlin5] p. 193 | Proposition 563Gb | nulmbl2 23304 |
| [Fremlin5] p. 213 | Lemma 565Ca | uniioovol 23347 |
| [Fremlin5] p. 214 | Lemma 565Ca | uniioombl 23357 |
| [Fremlin5] p. 218 | Lemma 565Ib | ftc1anclem6 33490 |
| [Fremlin5] p. 220 | Theorem 565Ma | ftc1anc 33493 |
| [FreydScedrov] p. 283 | Axiom of Infinity | ax-inf 8535 inf1 8519 inf2 8520 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 9733 enqer 9743 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nq 9738 df-nq 9734 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 9730 df-plq 9736 |
| [Gleason] p. 119 | Proposition 9-2.4 | caovmo 6871 df-mpq 9731 df-mq 9737 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 9739 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnq 9797 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 9798 ltbtwnnq 9800 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanq 9793 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnq 9794 |
| [Gleason] p. 120 | Proposition 9-2.6(iv) | ltrnq 9801 |
| [Gleason] p. 121 | Definition 9-3.1 | df-np 9803 |
| [Gleason] p. 121 | Definition 9-3.1 (ii) | prcdnq 9815 |
| [Gleason] p. 121 | Definition 9-3.1(iii) | prnmax 9817 |
| [Gleason] p. 122 | Definition | df-1p 9804 |
| [Gleason] p. 122 | Remark (1) | prub 9816 |
| [Gleason] p. 122 | Lemma 9-3.4 | prlem934 9855 |
| [Gleason] p. 122 | Proposition 9-3.2 | df-ltp 9807 |
| [Gleason] p. 122 | Proposition 9-3.3 | ltsopr 9854 psslinpr 9853 supexpr 9876 suplem1pr 9874 suplem2pr 9875 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 9840 addclprlem1 9838 addclprlem2 9839 df-plp 9805 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addasspr 9844 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcompr 9843 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 9856 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 9865 ltexprlem1 9858 ltexprlem2 9859 ltexprlem3 9860 ltexprlem4 9861 ltexprlem5 9862 ltexprlem6 9863 ltexprlem7 9864 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltapr 9867 ltaprlem 9866 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanpr 9868 |
| [Gleason] p. 124 | Lemma 9-3.6 | prlem936 9869 |
| [Gleason] p. 124 | Proposition 9-3.7 | df-mp 9806 mulclpr 9842 mulclprlem 9841 reclem2pr 9870 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 9851 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulasspr 9846 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcompr 9845 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrpr 9850 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 9873 reclem3pr 9871 reclem4pr 9872 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 9877 enrer 9886 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 9882 df-1r 9883 df-nr 9878 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 9880 df-plr 9879 negexsr 9923 recexsr 9928 recexsrlem 9924 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 9881 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 11015 creur 11014 cru 11012 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 10009 axcnre 9985 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 13855 crimd 13972 crimi 13933 crre 13854 crred 13971 crrei 13932 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 13857 remimd 13938 |
| [Gleason] p. 133 | Definition 10.36 | absval2 14024 absval2d 14184 absval2i 14136 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 13881 cjaddd 13960 cjaddi 13928 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 13882 cjmuld 13961 cjmuli 13929 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 13880 cjcjd 13939 cjcji 13911 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 13879 cjreb 13863 cjrebd 13942 cjrebi 13914 cjred 13966 rere 13862 rereb 13860 rerebd 13941 rerebi 13913 rered 13964 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 13888 addcjd 13952 addcji 13923 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 13978 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 14019 abscjd 14189 abscji 14140 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 14029 abs00d 14185 abs00i 14137 absne0d 14186 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 14061 releabsd 14190 releabsi 14141 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 14034 absmuld 14193 absmuli 14143 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 14022 sqabsaddi 14144 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 14070 abstrid 14195 abstrii 14147 |
| [Gleason] p. 134 | Definition 10-4.1 | 0exp0e1 12865 df-exp 12861 exp0 12864 expp1 12867 expp1d 13009 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | cxpadd 24425 cxpaddd 24463 expadd 12902 expaddd 13010 expaddz 12904 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 24434 cxpmuld 24480 expmul 12905 expmuld 13011 expmulz 12906 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulcxp 24431 mulcxpd 24474 mulexp 12899 mulexpd 13023 mulexpz 12900 |
| [Gleason] p. 140 | Exercise 1 | znnen 14941 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 12328 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 14362 rlimadd 14373 rlimdiv 14376 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 14364 rlimsub 14374 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 14363 rlimmul 14375 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 14367 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 14314 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 14334 climcj 14335 climim 14337 climre 14336 rlimabs 14339 rlimcj 14340 rlimim 14342 rlimre 14341 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 10079 df-xr 10078 ltxr 11949 |
| [Gleason] p. 175 | Definition 12-4.1 | df-limsup 14202 limsupval 14205 |
| [Gleason] p. 180 | Theorem 12-5.1 | climsup 14400 |
| [Gleason] p. 180 | Theorem 12-5.3 | caucvg 14409 caucvgb 14410 caucvgr 14406 climcau 14401 |
| [Gleason] p. 182 | Exercise 3 | cvgcmp 14548 |
| [Gleason] p. 182 | Exercise 4 | cvgrat 14615 |
| [Gleason] p. 195 | Theorem 13-2.12 | abs1m 14075 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 12629 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 19740 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 22148 xmet0 22147 |
| [Gleason] p. 223 | Definition 14-1.1(b) | metgt0 22164 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 22155 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 22157 mstri 22274 xmettri 22156 xmstri 22273 |
| [Gleason] p. 225 | Definition 14-1.5 | xpsmet 22187 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 21451 |
| [Gleason] p. 240 | Theorem 14-4.3 | metcnp4 23108 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 22345 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn 22668 addcn2 14324 mulcn 22670 mulcn2 14326 subcn 22669 subcn2 14325 |
| [Gleason] p. 295 | Remark | bcval3 13093 bcval4 13094 |
| [Gleason] p. 295 | Equation 2 | bcpasc 13108 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 13091 df-bc 13090 |
| [Gleason] p. 296 | Remark | bcn0 13097 bcnn 13099 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 14562 |
| [Gleason] p. 308 | Equation 2 | ef0 14821 |
| [Gleason] p. 308 | Equation 3 | efcj 14822 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 14827 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 14831 |
| [Gleason] p. 310 | Equation 14 | sinadd 14894 |
| [Gleason] p. 310 | Equation 15 | cosadd 14895 |
| [Gleason] p. 311 | Equation 17 | sincossq 14906 |
| [Gleason] p. 311 | Equation 18 | cosbnd 14911 sinbnd 14910 |
| [Gleason] p. 311 | Lemma 15-4.7 | sqeqor 12978 sqeqori 12976 |
| [Gleason] p. 311 | Definition of pi | df-pi 14803 |
| [Godowski] p. 730 | Equation SF | goeqi 29132 |
| [GodowskiGreechie] p. 249 | Equation IV | 3oai 28527 |
| [Golan] p. 1 | Remark | srgisid 18528 |
| [Golan] p. 1 | Definition | df-srg 18506 |
| [Golan] p. 149 | Definition | df-slmd 29754 |
| [GramKnuthPat], p. 47 | Definition 2.42 | df-fwddif 32266 |
| [Gratzer] p. 23 | Section 0.6 | df-mre 16246 |
| [Gratzer] p. 27 | Section 0.6 | df-mri 16248 |
| [Hall] p. 1 | Section 1.1 | df-asslaw 41824 df-cllaw 41822 df-comlaw 41823 |
| [Hall] p. 2 | Section 1.2 | df-clintop 41836 |
| [Hall] p. 7 | Section 1.3 | df-sgrp2 41857 |
| [Halmos] p. 31 | Theorem 17.3 | riesz1 28924 riesz2 28925 |
| [Halmos] p. 41 | Definition of Hermitian | hmopadj2 28800 |
| [Halmos] p. 42 | Definition of projector ordering | pjordi 29032 |
| [Halmos] p. 43 | Theorem 26.1 | elpjhmop 29044 elpjidm 29043 pjnmopi 29007 |
| [Halmos] p. 44 | Remark | pjinormi 28546 pjinormii 28535 |
| [Halmos] p. 44 | Theorem 26.2 | elpjch 29048 pjrn 28566 pjrni 28561 pjvec 28555 |
| [Halmos] p. 44 | Theorem 26.3 | pjnorm2 28586 |
| [Halmos] p. 44 | Theorem 26.4 | hmopidmpj 29013 hmopidmpji 29011 |
| [Halmos] p. 45 | Theorem 27.1 | pjinvari 29050 |
| [Halmos] p. 45 | Theorem 27.3 | pjoci 29039 pjocvec 28556 |
| [Halmos] p. 45 | Theorem 27.4 | pjorthcoi 29028 |
| [Halmos] p. 48 | Theorem 29.2 | pjssposi 29031 |
| [Halmos] p. 48 | Theorem 29.3 | pjssdif1i 29034 pjssdif2i 29033 |
| [Halmos] p. 50 | Definition of spectrum | df-spec 28714 |
| [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 1722 |
| [Hatcher] p. 25 | Definition | df-phtpc 22791 df-phtpy 22770 |
| [Hatcher] p. 26 | Definition | df-pco 22805 df-pi1 22808 |
| [Hatcher] p. 26 | Proposition 1.2 | phtpcer 22794 |
| [Hatcher] p. 26 | Proposition 1.3 | pi1grp 22850 |
| [Hefferon] p. 240 | Definition 3.12 | df-dmat 20296 df-dmatalt 42187 |
| [Helfgott] p. 2 | Theorem | tgoldbach 41705 |
| [Helfgott] p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 41690 |
| [Helfgott] p. 4 | Section 1.2.2 | ax-hgprmladder 41702 bgoldbtbnd 41697 bgoldbtbnd 41697 tgblthelfgott 41703 |
| [Helfgott] p. 5 | Proposition 1.1 | circlevma 30720 |
| [Helfgott] p. 69 | Statement 7.49 | circlemethhgt 30721 |
| [Helfgott] p. 69 | Statement 7.50 | hgt750lema 30735 hgt750lemb 30734 hgt750leme 30736 hgt750lemf 30731 hgt750lemg 30732 |
| [Helfgott] p. 70 | Section 7.4 | ax-tgoldbachgt 41699 tgoldbachgt 30741 tgoldbachgtALTV 41700 tgoldbachgtd 30740 |
| [Helfgott] p. 70 | Statement 7.49 | ax-hgt749 30722 |
| [Herstein] p. 54 | Exercise 28 | df-grpo 27347 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 17433 grpoideu 27363 mndideu 17304 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 17456 grpoinveu 27373 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 17482 grpo2inv 27385 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 17493 grpoinvop 27387 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3e 17515 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1693 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1694 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1696 |
| [Holland] p. 1519 | Theorem 2 | sumdmdi 29279 |
| [Holland] p. 1520 | Lemma 5 | cdj1i 29292 cdj3i 29300 cdj3lem1 29293 cdjreui 29291 |
| [Holland] p. 1524 | Lemma 7 | mddmdin0i 29290 |
| [Holland95] p. 13 | Theorem 3.6 | hlathil 37253 |
| [Holland95] p. 14 | Line 15 | hgmapvs 37183 |
| [Holland95] p. 14 | Line 16 | hdmaplkr 37205 |
| [Holland95] p. 14 | Line 17 | hdmapellkr 37206 |
| [Holland95] p. 14 | Line 19 | hdmapglnm2 37203 |
| [Holland95] p. 14 | Line 20 | hdmapip0com 37209 |
| [Holland95] p. 14 | Theorem 3.6 | hdmapevec2 37128 |
| [Holland95] p. 14 | Lines 24 and 25 | hdmapoc 37223 |
| [Holland95] p. 204 | Definition of involution | df-srng 18846 |
| [Holland95] p. 212 | Definition of subspace | df-psubsp 34789 |
| [Holland95] p. 214 | Lemma 3.3 | lclkrlem2v 36817 |
| [Holland95] p. 214 | Definition 3.2 | df-lpolN 36770 |
| [Holland95] p. 214 | Definition of nonsingular | pnonsingN 35219 |
| [Holland95] p. 215 | Lemma 3.3(1) | dihoml4 36666 poml4N 35239 |
| [Holland95] p. 215 | Lemma 3.3(2) | dochexmid 36757 pexmidALTN 35264 pexmidN 35255 |
| [Holland95] p. 218 | Theorem 3.6 | lclkr 36822 |
| [Holland95] p. 218 | Definition of dual vector space | df-ldual 34411 ldualset 34412 |
| [Holland95] p. 222 | Item 1 | df-lines 34787 df-pointsN 34788 |
| [Holland95] p. 222 | Item 2 | df-polarityN 35189 |
| [Holland95] p. 223 | Remark | ispsubcl2N 35233 omllaw4 34533 pol1N 35196 polcon3N 35203 |
| [Holland95] p. 223 | Definition | df-psubclN 35221 |
| [Holland95] p. 223 | Equation for polarity | polval2N 35192 |
| [Holmes] p. 40 | Definition | df-xrn 34134 |
| [Hughes] p. 44 | Equation 1.21b | ax-his3 27941 |
| [Hughes] p. 47 | Definition of projection operator | dfpjop 29041 |
| [Hughes] p. 49 | Equation 1.30 | eighmre 28822 eigre 28694 eigrei 28693 |
| [Hughes] p. 49 | Equation 1.31 | eighmorth 28823 eigorth 28697 eigorthi 28696 |
| [Hughes] p. 137 | Remark (ii) | eigposi 28695 |
| [Huneke] p. 1 | Claim 1 | frgrncvvdeq 27173 |
| [Huneke] p. 1 | Statement 1 | frgrncvvdeqlem7 27169 |
| [Huneke] p. 1 | Statement 2 | frgrncvvdeqlem8 27170 |
| [Huneke] p. 1 | Statement 3 | frgrncvvdeqlem9 27171 |
| [Huneke] p. 2 | Claim 2 | frgrregorufr 27189 frgrregorufr0 27188 frgrregorufrg 27190 |
| [Huneke] p. 2 | Claim 3 | frgrhash2wsp 27196 frrusgrord 27205 frrusgrord0 27204 |
| [Huneke] p. 2 | Statement 4 | frgrwopreglem4 27179 |
| [Huneke] p. 2 | Statement 5 | frgrwopreg1 27182 frgrwopreg2 27183 frgrwopregasn 27180 frgrwopregbsn 27181 |
| [Huneke] p. 2 | Statement 6 | frgrwopreglem5 27185 |
| [Huneke] p. 2 | Statement 7 | fusgreghash2wspv 27199 |
| [Huneke] p. 2 | Statement 8 | fusgreghash2wsp 27202 |
| [Huneke] p. 2 | Statement 9 | clwlksndivn 26972 numclwwlk1 27231 numclwwlk8 27250 |
| [Huneke] p. 2 | Definition 3 | frgrwopreglem1 27176 |
| [Huneke] p. 2 | Definition 4 | df-clwlks 26667 |
| [Huneke] p. 2 | Definition 5 | numclwwlkovf 27213 |
| [Huneke] p. 2 | Definition 6 | numclwwlkovg 27220 |
| [Huneke] p. 2 | Definition 7 | numclwwlkovh 27234 |
| [Huneke] p. 2 | Statement 10 | numclwwlk2 27240 |
| [Huneke] p. 2 | Statement 11 | rusgrnumwlkg 26872 |
| [Huneke] p. 2 | Statement 12 | numclwwlk3 27243 |
| [Huneke] p. 2 | Statement 13 | numclwwlk5 27246 |
| [Huneke] p. 2 | Statement 14 | numclwwlk7 27249 |
| [Indrzejczak] p. 33 | Definition ` `E | natded 27260 natded 27260 |
| [Indrzejczak] p. 33 | Definition ` `I | natded 27260 |
| [Indrzejczak] p. 34 | Definition ` `E | natded 27260 natded 27260 |
| [Indrzejczak] p. 34 | Definition ` `I | natded 27260 |
| [Jech] p. 4 | Definition of class | cv 1482 cvjust 2617 |
| [Jech] p. 42 | Lemma 6.1 | alephexp1 9401 |
| [Jech] p. 42 | Equation 6.1 | alephadd 9399 alephmul 9400 |
| [Jech] p. 43 | Lemma 6.2 | infmap 9398 infmap2 9040 |
| [Jech] p. 71 | Lemma 9.3 | jech9.3 8677 |
| [Jech] p. 72 | Equation 9.3 | scott0 8749 scottex 8748 |
| [Jech] p. 72 | Exercise 9.1 | rankval4 8730 |
| [Jech] p. 72 | Scheme "Collection Principle" | cp 8754 |
| [Jech] p. 78 | Note | opthprc 5167 |
| [JonesMatijasevic] p. 694 | Definition 2.3 | rmxyval 37480 |
| [JonesMatijasevic] p. 695 | Lemma 2.15 | jm2.15nn0 37570 |
| [JonesMatijasevic] p. 695 | Lemma 2.16 | jm2.16nn0 37571 |
| [JonesMatijasevic] p. 695 | Equation 2.7 | rmxadd 37492 |
| [JonesMatijasevic] p. 695 | Equation 2.8 | rmyadd 37496 |
| [JonesMatijasevic] p. 695 | Equation 2.9 | rmxp1 37497 rmyp1 37498 |
| [JonesMatijasevic] p. 695 | Equation 2.10 | rmxm1 37499 rmym1 37500 |
| [JonesMatijasevic] p. 695 | Equation 2.11 | rmx0 37490 rmx1 37491 rmxluc 37501 |
| [JonesMatijasevic] p. 695 | Equation 2.12 | rmy0 37494 rmy1 37495 rmyluc 37502 |
| [JonesMatijasevic] p. 695 | Equation 2.13 | rmxdbl 37504 |
| [JonesMatijasevic] p. 695 | Equation 2.14 | rmydbl 37505 |
| [JonesMatijasevic] p. 696 | Lemma 2.17 | jm2.17a 37527 jm2.17b 37528 jm2.17c 37529 |
| [JonesMatijasevic] p. 696 | Lemma 2.19 | jm2.19 37560 |
| [JonesMatijasevic] p. 696 | Lemma 2.20 | jm2.20nn 37564 |
| [JonesMatijasevic] p. 696 | Theorem 2.18 | jm2.18 37555 |
| [JonesMatijasevic] p. 697 | Lemma 2.24 | jm2.24 37530 jm2.24nn 37526 |
| [JonesMatijasevic] p. 697 | Lemma 2.26 | jm2.26 37569 |
| [JonesMatijasevic] p. 697 | Lemma 2.27 | jm2.27 37575 rmygeid 37531 |
| [JonesMatijasevic] p. 698 | Lemma 3.1 | jm3.1 37587 |
| [Juillerat] p. 11 | Section *5 | etransc 40500 etransclem47 40498 etransclem48 40499 |
| [Juillerat] p. 12 | Equation (7) | etransclem44 40495 |
| [Juillerat] p. 12 | Equation *(7) | etransclem46 40497 |
| [Juillerat] p. 12 | Proof of the derivative calculated | etransclem32 40483 |
| [Juillerat] p. 13 | Proof | etransclem35 40486 |
| [Juillerat] p. 13 | Part of case 2 proven in | etransclem38 40489 |
| [Juillerat] p. 13 | Part of case 2 proven | etransclem24 40475 |
| [Juillerat] p. 13 | Part of case 2: proven in | etransclem41 40492 |
| [Juillerat] p. 14 | Proof | etransclem23 40474 |
| [KalishMontague] p. 81 | Note 1 | ax-6 1888 |
| [KalishMontague] p. 85 | Lemma 2 | equid 1939 |
| [KalishMontague] p. 85 | Lemma 3 | equcomi 1944 |
| [KalishMontague] p. 86 | Lemma 7 | cbvalivw 1934 cbvaliw 1933 |
| [KalishMontague] p. 87 | Lemma 8 | spimvw 1927 spimw 1926 |
| [KalishMontague] p. 87 | Lemma 9 | spfw 1965 spw 1967 |
| [Kalmbach] p. 14 | Definition of lattice | chabs1 28375 chabs1i 28377 chabs2 28376 chabs2i 28378 chjass 28392 chjassi 28345 latabs1 17087 latabs2 17088 |
| [Kalmbach] p. 15 | Definition of atom | df-at 29197 ela 29198 |
| [Kalmbach] p. 15 | Definition of covers | cvbr2 29142 cvrval2 34561 |
| [Kalmbach] p. 16 | Definition | df-ol 34465 df-oml 34466 |
| [Kalmbach] p. 20 | Definition of commutes | cmbr 28443 cmbri 28449 cmtvalN 34498 df-cm 28442 df-cmtN 34464 |
| [Kalmbach] p. 22 | Remark | omllaw5N 34534 pjoml5 28472 pjoml5i 28447 |
| [Kalmbach] p. 22 | Definition | pjoml2 28470 pjoml2i 28444 |
| [Kalmbach] p. 22 | Theorem 2(v) | cmcm 28473 cmcmi 28451 cmcmii 28456 cmtcomN 34536 |
| [Kalmbach] p. 22 | Theorem 2(ii) | omllaw3 34532 omlsi 28263 pjoml 28295 pjomli 28294 |
| [Kalmbach] p. 22 | Definition of OML law | omllaw2N 34531 |
| [Kalmbach] p. 23 | Remark | cmbr2i 28455 cmcm3 28474 cmcm3i 28453 cmcm3ii 28458 cmcm4i 28454 cmt3N 34538 cmt4N 34539 cmtbr2N 34540 |
| [Kalmbach] p. 23 | Lemma 3 | cmbr3 28467 cmbr3i 28459 cmtbr3N 34541 |
| [Kalmbach] p. 25 | Theorem 5 | fh1 28477 fh1i 28480 fh2 28478 fh2i 28481 omlfh1N 34545 |
| [Kalmbach] p. 65 | Remark | chjatom 29216 chslej 28357 chsleji 28317 shslej 28239 shsleji 28229 |
| [Kalmbach] p. 65 | Proposition 1 | chocin 28354 chocini 28313 chsupcl 28199 chsupval2 28269 h0elch 28112 helch 28100 hsupval2 28268 ocin 28155 ococss 28152 shococss 28153 |
| [Kalmbach] p. 65 | Definition of subspace sum | shsval 28171 |
| [Kalmbach] p. 66 | Remark | df-pjh 28254 pjssmi 29024 pjssmii 28540 |
| [Kalmbach] p. 67 | Lemma 3 | osum 28504 osumi 28501 |
| [Kalmbach] p. 67 | Lemma 4 | pjci 29059 |
| [Kalmbach] p. 103 | Exercise 6 | atmd2 29259 |
| [Kalmbach] p. 103 | Exercise 12 | mdsl0 29169 |
| [Kalmbach] p. 140 | Remark | hatomic 29219 hatomici 29218 hatomistici 29221 |
| [Kalmbach] p. 140 | Proposition 1 | atlatmstc 34606 |
| [Kalmbach] p. 140 | Proposition 1(i) | atexch 29240 lsatexch 34330 |
| [Kalmbach] p. 140 | Proposition 1(ii) | chcv1 29214 cvlcvr1 34626 cvr1 34696 |
| [Kalmbach] p. 140 | Proposition 1(iii) | cvexch 29233 cvexchi 29228 cvrexch 34706 |
| [Kalmbach] p. 149 | Remark 2 | chrelati 29223 hlrelat 34688 hlrelat5N 34687 lrelat 34301 |
| [Kalmbach] p. 153 | Exercise 5 | lsmcv 19141 lsmsatcv 34297 spansncv 28512 spansncvi 28511 |
| [Kalmbach] p. 153 | Proposition 1(ii) | lsmcv2 34316 spansncv2 29152 |
| [Kalmbach] p. 266 | Definition | df-st 29070 |
| [Kalmbach2] p. 8 | Definition of adjoint | df-adjh 28708 |
| [KanamoriPincus] p. 415 | Theorem 1.1 | fpwwe 9468 fpwwe2 9465 |
| [KanamoriPincus] p. 416 | Corollary 1.3 | canth4 9469 |
| [KanamoriPincus] p. 417 | Corollary 1.6 | canthp1 9476 |
| [KanamoriPincus] p. 417 | Corollary 1.4(a) | canthnum 9471 |
| [KanamoriPincus] p. 417 | Corollary 1.4(b) | canthwe 9473 |
| [KanamoriPincus] p. 418 | Proposition 1.7 | pwfseq 9486 |
| [KanamoriPincus] p. 419 | Lemma 2.2 | gchcdaidm 9490 gchxpidm 9491 |
| [KanamoriPincus] p. 419 | Theorem 2.1 | gchacg 9502 gchhar 9501 |
| [KanamoriPincus] p. 420 | Lemma 2.3 | pwcdadom 9038 unxpwdom 8494 |
| [KanamoriPincus] p. 421 | Proposition 3.1 | gchpwdom 9492 |
| [Kreyszig] p. 3 | Property M1 | metcl 22137 xmetcl 22136 |
| [Kreyszig] p. 4 | Property M2 | meteq0 22144 |
| [Kreyszig] p. 8 | Definition 1.1-8 | dscmet 22377 |
| [Kreyszig] p. 12 | Equation 5 | conjmul 10742 muleqadd 10671 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 22243 |
| [Kreyszig] p. 19 | Remark | mopntopon 22244 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 22303 mopnm 22249 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 22301 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 22306 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 22347 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 21062 lmmbr 23056 lmmbr2 23057 |
| [Kreyszig] p. 26 | Lemma 1.4-2(a) | lmmo 21184 |
| [Kreyszig] p. 28 | Theorem 1.4-5 | lmcau 23111 |
| [Kreyszig] p. 28 | Definition 1.4-3 | iscau 23074 iscmet2 23092 |
| [Kreyszig] p. 30 | Theorem 1.4-7 | cmetss 23113 |
| [Kreyszig] p. 30 | Theorem 1.4-6(a) | 1stcelcls 21264 metelcls 23103 |
| [Kreyszig] p. 30 | Theorem 1.4-6(b) | metcld 23104 metcld2 23105 |
| [Kreyszig] p. 51 | Equation 2 | clmvneg1 22899 lmodvneg1 18906 nvinv 27494 vcm 27431 |
| [Kreyszig] p. 51 | Equation 1a | clm0vs 22895 lmod0vs 18896 slmd0vs 29777 vc0 27429 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 18897 slmdvs0 29778 vcz 27430 |
| [Kreyszig] p. 58 | Definition 2.2-1 | imsmet 27546 ngpmet 22407 nrmmetd 22379 |
| [Kreyszig] p. 59 | Equation 1 | imsdval 27541 imsdval2 27542 ncvspds 22961 ngpds 22408 |
| [Kreyszig] p. 63 | Problem 1 | nmval 22394 nvnd 27543 |
| [Kreyszig] p. 64 | Problem 2 | nmeq0 22422 nmge0 22421 nvge0 27528 nvz 27524 |
| [Kreyszig] p. 64 | Problem 3 | nmrtri 22428 nvabs 27527 |
| [Kreyszig] p. 91 | Definition 2.7-1 | isblo3i 27656 |
| [Kreyszig] p. 92 | Equation 2 | df-nmoo 27600 |
| [Kreyszig] p. 97 | Theorem 2.7-9(a) | blocn 27662 blocni 27660 |
| [Kreyszig] p. 97 | Theorem 2.7-9(b) | lnocni 27661 |
| [Kreyszig] p. 129 | Definition 3.1-1 | cphipeq0 23004 ipeq0 19983 ipz 27574 |
| [Kreyszig] p. 135 | Problem 2 | pythi 27705 |
| [Kreyszig] p. 137 | Lemma 3-2.1(a) | sii 27709 |
| [Kreyszig] p. 144 | Equation 4 | supcvg 14588 |
| [Kreyszig] p. 144 | Theorem 3.3-1 | minvec 23207 minveco 27740 |
| [Kreyszig] p. 196 | Definition 3.9-1 | df-aj 27605 |
| [Kreyszig] p. 247 | Theorem 4.7-2 | bcth 23126 |
| [Kreyszig] p. 249 | Theorem 4.7-3 | ubth 27729 |
| [Kreyszig] p. 470 | Definition of positive operator ordering | leop 28982 leopg 28981 |
| [Kreyszig] p. 476 | Theorem 9.4-2 | opsqrlem2 29000 |
| [Kreyszig] p. 525 | Theorem 10.1-1 | htth 27775 |
| [Kulpa] p. 547 | Theorem | poimir 33442 |
| [Kulpa] p. 547 | Equation (1) | poimirlem32 33441 |
| [Kulpa] p. 547 | Equation (2) | poimirlem31 33440 |
| [Kulpa] p. 548 | Theorem | broucube 33443 |
| [Kulpa] p. 548 | Equation (6) | poimirlem26 33435 |
| [Kulpa] p. 548 | Equation (7) | poimirlem27 33436 |
| [Kunen] p. 10 | Axiom 0 | ax6e 2250 axnul 4788 |
| [Kunen] p. 11 | Axiom 3 | axnul 4788 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 7134 |
| [Kunen] p. 24 | Definition 10.24 | mapval 7869 mapvalg 7867 |
| [Kunen] p. 30 | Lemma 10.20 | fodom 9344 |
| [Kunen] p. 31 | Definition 10.24 | mapex 7863 |
| [Kunen] p. 95 | Definition 2.1 | df-r1 8627 |
| [Kunen] p. 97 | Lemma 2.10 | r1elss 8669 r1elssi 8668 |
| [Kunen] p. 107 | Exercise 4 | rankop 8721 rankopb 8715 rankuni 8726 rankxplim 8742 rankxpsuc 8745 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4531 |
| [Lang] p. 3 | Definition | df-mnd 17295 |
| [Lang] p. 7 | Definition | dfgrp2e 17448 |
| [Lang] p. 53 | Definition | df-cat 16329 |
| [Lang] p. 54 | Definition | df-iso 16409 |
| [Lang] p. 57 | Definition | df-inito 16641 df-termo 16642 |
| [Lang] p. 58 | Example | irinitoringc 42069 |
| [Lang] p. 58 | Statement | initoeu1 16661 termoeu1 16668 |
| [Lang] p. 62 | Definition | df-func 16518 |
| [Lang] p. 65 | Definition | df-nat 16603 |
| [Lang] p. 91 | Note | df-ringc 42005 |
| [Lang] p. 128 | Remark | dsmmlmod 20089 |
| [Lang] p. 129 | Proof | lincscm 42219 lincscmcl 42221 lincsum 42218 lincsumcl 42220 |
| [Lang] p. 129 | Statement | lincolss 42223 |
| [Lang] p. 129 | Observation | dsmmfi 20082 |
| [Lang] p. 147 | Definition | snlindsntor 42260 |
| [Lang] p. 504 | Statement | mat1 20253 matring 20249 |
| [Lang] p. 504 | Definition | df-mamu 20190 |
| [Lang] p. 505 | Statement | mamuass 20208 mamutpos 20264 matassa 20250 mattposvs 20261 tposmap 20263 |
| [Lang] p. 513 | Definition | mdet1 20407 mdetf 20401 |
| [Lang] p. 513 | Theorem 4.4 | cramer 20497 |
| [Lang] p. 514 | Proposition 4.6 | mdetleib 20393 |
| [Lang] p. 514 | Proposition 4.8 | mdettpos 20417 |
| [Lang] p. 515 | Definition | df-minmar1 20441 smadiadetr 20481 |
| [Lang] p. 515 | Corollary 4.9 | mdetero 20416 mdetralt 20414 |
| [Lang] p. 517 | Proposition 4.15 | mdetmul 20429 |
| [Lang] p. 518 | Definition | df-madu 20440 |
| [Lang] p. 518 | Proposition 4.16 | madulid 20451 madurid 20450 matinv 20483 |
| [Lang] p. 561 | Theorem 3.1 | cayleyhamilton 20695 |
| [Lang], p. 561 | Remark | chpmatply1 20637 |
| [Lang], p. 561 | Definition | df-chpmat 20632 |
| [LarsonHostetlerEdwards] p. 278 | Section 4.1 | dvconstbi 38533 |
| [LarsonHostetlerEdwards] p. 311 | Example 1a | lhe4.4ex1a 38528 |
| [LarsonHostetlerEdwards] p. 375 | Theorem 5.1 | expgrowth 38534 |
| [LeBlanc] p. 277 | Rule R2 | axnul 4788 |
| [Levy] p. 338 | Axiom | df-clab 2609 df-clel 2618 df-cleq 2615 |
| [Levy58] p. 2 | Definition I | isfin1-3 9208 |
| [Levy58] p. 2 | Definition II | df-fin2 9108 |
| [Levy58] p. 2 | Definition Ia | df-fin1a 9107 |
| [Levy58] p. 2 | Definition III | df-fin3 9110 |
| [Levy58] p. 3 | Definition V | df-fin5 9111 |
| [Levy58] p. 3 | Definition IV | df-fin4 9109 |
| [Levy58] p. 4 | Definition VI | df-fin6 9112 |
| [Levy58] p. 4 | Definition VII | df-fin7 9113 |
| [Levy58], p. 3 | Theorem 1 | fin1a2 9237 |
| [Lipparini] p. 3 | Lemma 2.1.1 | nosepssdm 31836 |
| [Lipparini] p. 3 | Lemma 2.1.4 | noresle 31846 |
| [Lipparini] p. 6 | Proposition 4.2 | nosupbnd1 31860 |
| [Lipparini] p. 6 | Proposition 4.3 | nosupbnd2 31862 |
| [Lipparini] p. 7 | Theorem 5.1 | noetalem2 31864 noetalem3 31865 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1693 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1694 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1696 |
| [Maeda] p. 167 | Theorem 1(d) to (e) | mdsymlem6 29267 |
| [Maeda] p. 168 | Lemma 5 | mdsym 29271 mdsymi 29270 |
| [Maeda] p. 168 | Lemma 4(i) | mdsymlem4 29265 mdsymlem6 29267 mdsymlem7 29268 |
| [Maeda] p. 168 | Lemma 4(ii) | mdsymlem8 29269 |
| [MaedaMaeda] p. 1 | Remark | ssdmd1 29172 ssdmd2 29173 ssmd1 29170 ssmd2 29171 |
| [MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 29168 |
| [MaedaMaeda] p. 1 | Definition 1.1 | df-dmd 29140 df-md 29139 mdbr 29153 |
| [MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 29190 mdslj1i 29178 mdslj2i 29179 mdslle1i 29176 mdslle2i 29177 mdslmd1i 29188 mdslmd2i 29189 |
| [MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 29180 mdsl2bi 29182 mdsl2i 29181 |
| [MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 29194 |
| [MaedaMaeda] p. 2 | Lemma 1.5.1 | mdslmd3i 29191 |
| [MaedaMaeda] p. 2 | Lemma 1.5.2 | mdslmd4i 29192 |
| [MaedaMaeda] p. 2 | Lemma 1.5.3 | mdsl0 29169 |
| [MaedaMaeda] p. 2 | Theorem 1.3 | dmdsl3 29174 mdsl3 29175 |
| [MaedaMaeda] p. 3 | Theorem 1.9.1 | csmdsymi 29193 |
| [MaedaMaeda] p. 4 | Theorem 1.14 | mdcompli 29288 |
| [MaedaMaeda] p. 30 | Lemma 7.2 | atlrelat1 34608 hlrelat1 34686 |
| [MaedaMaeda] p. 31 | Lemma 7.5 | lcvexch 34326 |
| [MaedaMaeda] p. 31 | Lemma 7.5.1 | cvmd 29195 cvmdi 29183 cvnbtwn4 29148 cvrnbtwn4 34566 |
| [MaedaMaeda] p. 31 | Lemma 7.5.2 | cvdmd 29196 |
| [MaedaMaeda] p. 31 | Definition 7.4 | cvlcvrp 34627 cvp 29234 cvrp 34702 lcvp 34327 |
| [MaedaMaeda] p. 31 | Theorem 7.6(b) | atmd 29258 |
| [MaedaMaeda] p. 31 | Theorem 7.6(c) | atdmd 29257 |
| [MaedaMaeda] p. 32 | Definition 7.8 | cvlexch4N 34620 hlexch4N 34678 |
| [MaedaMaeda] p. 34 | Exercise 7.1 | atabsi 29260 |
| [MaedaMaeda] p. 41 | Lemma 9.2(delta) | cvrat4 34729 |
| [MaedaMaeda] p. 61 | Definition 15.1 | 0psubN 35035 atpsubN 35039 df-pointsN 34788 pointpsubN 35037 |
| [MaedaMaeda] p. 62 | Theorem 15.5 | df-pmap 34790 pmap11 35048 pmaple 35047 pmapsub 35054 pmapval 35043 |
| [MaedaMaeda] p. 62 | Theorem 15.5.1 | pmap0 35051 pmap1N 35053 |
| [MaedaMaeda] p. 62 | Theorem 15.5.2 | pmapglb 35056 pmapglb2N 35057 pmapglb2xN 35058 pmapglbx 35055 |
| [MaedaMaeda] p. 63 | Equation 15.5.3 | pmapjoin 35138 |
| [MaedaMaeda] p. 67 | Postulate PS1 | ps-1 34763 |
| [MaedaMaeda] p. 68 | Lemma 16.2 | df-padd 35082 paddclN 35128 paddidm 35127 |
| [MaedaMaeda] p. 68 | Condition PS2 | ps-2 34764 |
| [MaedaMaeda] p. 68 | Equation 16.2.1 | paddass 35124 |
| [MaedaMaeda] p. 69 | Lemma 16.4 | ps-1 34763 |
| [MaedaMaeda] p. 69 | Theorem 16.4 | ps-2 34764 |
| [MaedaMaeda] p. 70 | Theorem 16.9 | lsmmod 18088 lsmmod2 18089 lssats 34299 shatomici 29217 shatomistici 29220 shmodi 28249 shmodsi 28248 |
| [MaedaMaeda] p. 130 | Remark 29.6 | dmdmd 29159 mdsymlem7 29268 |
| [MaedaMaeda] p. 132 | Theorem 29.13(e) | pjoml6i 28448 |
| [MaedaMaeda] p. 136 | Lemma 31.1.5 | shjshseli 28352 |
| [MaedaMaeda] p. 139 | Remark | sumdmdii 29274 |
| [Margaris] p. 40 | Rule C | exlimiv 1858 |
| [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 386 df-ex 1705 df-or 385 dfbi2 660 |
| [Margaris] p. 51 | Theorem 1 | idALT 23 |
| [Margaris] p. 56 | Theorem 3 | conventions 27258 |
| [Margaris] p. 59 | Section 14 | notnotrALTVD 39151 |
| [Margaris] p. 60 | Theorem 8 | mth8 158 |
| [Margaris] p. 60 | Section 14 | con3ALTVD 39152 |
| [Margaris] p. 79 | Rule C | exinst01 38850 exinst11 38851 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1892 19.2g 2058 r19.2z 4060 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 2069 rr19.3v 3345 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 2037 |
| [Margaris] p. 89 | Theorem 19.6 | alex 1753 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1706 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 2052 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 2072 19.9h 2120 exlimd 2087 exlimdh 2149 |
| [Margaris] p. 89 | Theorem 19.11 | excom 2042 excomim 2043 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 2164 |
| [Margaris] p. 90 | Section 19 | conventions-label 27259 conventions-label 27259 conventions-label 27259 conventions-label 27259 |
| [Margaris] p. 90 | Theorem 19.14 | exnal 1754 |
| [Margaris] p. 90 | Theorem 19.15 | 2albi 38577 albi 1746 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 2093 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 2094 |
| [Margaris] p. 90 | Theorem 19.18 | 2exbi 38579 exbi 1773 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 2097 |
| [Margaris] p. 90 | Theorem 19.20 | 2alim 38576 2alimdv 1847 alimd 2081 alimdh 1745 alimdv 1845 ax-4 1737 ralimdaa 2958 ralimdv 2963 ralimdva 2962 ralimdvva 2964 sbcimdv 3498 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21 2075 19.21h 2121 19.21t 2073 19.21vv 38575 alrimd 2084 alrimdd 2083 alrimdh 1790 alrimdv 1857 alrimi 2082 alrimih 1751 alrimiv 1855 alrimivv 1856 hbralrimi 2954 r19.21be 2933 r19.21bi 2932 ralrimd 2959 ralrimdv 2968 ralrimdva 2969 ralrimdvv 2973 ralrimdvva 2974 ralrimi 2957 ralrimia 39315 ralrimiv 2965 ralrimiva 2966 ralrimivv 2970 ralrimivva 2971 ralrimivvva 2972 ralrimivw 2967 |
| [Margaris] p. 90 | Theorem 19.22 | 2exim 38578 2eximdv 1848 exim 1761 eximd 2085 eximdh 1791 eximdv 1846 rexim 3008 reximd2a 3013 reximdai 3012 reximdd 39344 reximddv 3018 reximddv2 3020 reximddv3 39343 reximdv 3016 reximdv2 3014 reximdva 3017 reximdvai 3015 reximdvva 3019 reximi2 3010 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 2080 19.23bi 2061 19.23h 2122 exlimdv 1861 exlimdvv 1862 exlimexi 38730 exlimiv 1858 exlimivv 1860 rexlimd3 39335 rexlimdv 3030 rexlimdv3a 3033 rexlimdva 3031 rexlimdva2 39339 rexlimdvaa 3032 rexlimdvv 3037 rexlimdvva 3038 rexlimdvw 3034 rexlimiv 3027 rexlimiva 3028 rexlimivv 3036 |
| [Margaris] p. 90 | Theorem 19.24 | 19.24 1900 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1808 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26 1798 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 2095 r19.27z 4070 r19.27zv 4071 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 2096 19.28vv 38585 r19.28z 4063 r19.28zv 4066 rr19.28v 3346 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1801 r19.29d2r 3080 r19.29imd 3074 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30 1809 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31 2102 19.31vv 38583 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32 2101 r19.32 41167 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33-2 38581 19.33 1812 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1901 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35 1805 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36 2098 19.36vv 38582 r19.36zv 4072 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37 2100 19.37vv 38584 r19.37zv 4067 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1766 |
| [Margaris] p. 90 | Theorem 19.39 | 19.39 1899 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1814 19.40 1797 r19.40 3088 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 2103 19.41rg 38766 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 2105 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1810 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 2106 r19.44zv 4069 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 2107 r19.45zv 4068 |
| [Margaris] p. 90 | Theorem 1977.23 | 19.23t 2079 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2510 |
| [Mayet] p. 370 | Remark | jpi 29129 largei 29126 stri 29116 |
| [Mayet3] p. 9 | Definition of CH-states | df-hst 29071 ishst 29073 |
| [Mayet3] p. 10 | Theorem | hstrbi 29125 hstri 29124 |
| [Mayet3] p. 1223 | Theorem 4.1 | mayete3i 28587 |
| [Mayet3] p. 1240 | Theorem 7.1 | mayetes3i 28588 |
| [MegPav2000] p. 2344 | Theorem 3.3 | stcltrthi 29137 |
| [MegPav2000] p. 2345 | Definition 3.4-1 | chintcl 28191 chsupcl 28199 |
| [MegPav2000] p. 2345 | Definition 3.4-2 | hatomic 29219 |
| [MegPav2000] p. 2345 | Definition 3.4-3(a) | superpos 29213 |
| [MegPav2000] p. 2345 | Definition 3.4-3(b) | atexch 29240 |
| [MegPav2000] p. 2366 | Figure 7 | pl42N 35269 |
| [MegPav2002] p. 362 | Lemma 2.2 | latj31 17099 latj32 17097 latjass 17095 |
| [Megill] p. 444 | Axiom C5 | ax-5 1839 ax5ALT 34192 |
| [Megill] p. 444 | Section 7 | conventions 27258 |
| [Megill] p. 445 | Lemma L12 | aecom-o 34186 ax-c11n 34173 axc11n 2307 |
| [Megill] p. 446 | Lemma L17 | equtrr 1949 |
| [Megill] p. 446 | Lemma L18 | ax6fromc10 34181 |
| [Megill] p. 446 | Lemma L19 | hbnae-o 34213 hbnae 2317 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1881 sbid 2114 sbidd-misc 42460 sbidd 42459 |
| [Megill] p. 448 | Remark 9.6 | axc14 2372 |
| [Megill] p. 448 | Scheme C4' | ax-c4 34169 |
| [Megill] p. 448 | Scheme C5' | ax-c5 34168 sp 2053 |
| [Megill] p. 448 | Scheme C6' | ax-11 2034 |
| [Megill] p. 448 | Scheme C7' | ax-c7 34170 |
| [Megill] p. 448 | Scheme C8' | ax-7 1935 |
| [Megill] p. 448 | Scheme C9' | ax-c9 34175 |
| [Megill] p. 448 | Scheme C10' | ax-6 1888 ax-c10 34171 |
| [Megill] p. 448 | Scheme C11' | ax-c11 34172 |
| [Megill] p. 448 | Scheme C12' | ax-8 1992 |
| [Megill] p. 448 | Scheme C13' | ax-9 1999 |
| [Megill] p. 448 | Scheme C14' | ax-c14 34176 |
| [Megill] p. 448 | Scheme C15' | ax-c15 34174 |
| [Megill] p. 448 | Scheme C16' | ax-c16 34177 |
| [Megill] p. 448 | Theorem 9.4 | dral1-o 34189 dral1 2325 dral2-o 34215 dral2 2324 drex1 2327 drex2 2328 drsb1 2377 drsb2 2378 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2445 sbequ 2376 sbid2v 2457 |
| [Megill] p. 450 | Example in Appendix | hba1-o 34182 hba1 2151 |
| [Mendelson] p. 35 | Axiom A3 | hirstL-ax3 41059 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 23 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3518 rspsbca 3519 stdpc4 2353 |
| [Mendelson] p. 69 | Axiom 5 | ax-c4 34169 ra4 3525 stdpc5 2076 |
| [Mendelson] p. 81 | Rule C | exlimiv 1858 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1957 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1958 |
| [Mendelson] p. 225 | Axiom system NBG | ru 3434 |
| [Mendelson] p. 230 | Exercise 4.8(b) | opthwiener 4976 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3970 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3971 |
| [Mendelson] p. 231 | Exercise 4.10(n) | dfin3 3866 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3916 |
| [Mendelson] p. 231 | Exercise 4.10(q) | dfin4 3867 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddif 3742 |
| [Mendelson] p. 231 | Definition of union | dfun3 3865 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4919 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 4433 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 5018 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 5019 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssun 5020 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 4457 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 5249 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5656 |
| [Mendelson] p. 244 | Proposition 4.8(g) | epweon 6983 |
| [Mendelson] p. 246 | Definition of successor | df-suc 5729 |
| [Mendelson] p. 250 | Exercise 4.36 | oelim2 7675 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 8123 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 8044 xpsneng 8045 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 8051 xpcomeng 8052 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 8054 |
| [Mendelson] p. 255 | Definition | brsdom 7978 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 8047 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 7861 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 8035 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 8129 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 8128 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 7895 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 8036 |
| [Mendelson] p. 257 | Proposition 4.24(a) | undom 8048 |
| [Mendelson] p. 258 | Exercise 4.56(b) | cdaen 8995 |
| [Mendelson] p. 258 | Exercise 4.56(c) | cdaassen 9004 cdacomen 9003 |
| [Mendelson] p. 258 | Exercise 4.56(f) | cdadom1 9008 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2cda 9002 |
| [Mendelson] p. 258 | Definition of cardinal sum | cdaval 8992 df-cda 8990 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 7611 |
| [Mendelson] p. 266 | Proposition 4.34(f) | oaordex 7638 |
| [Mendelson] p. 275 | Proposition 4.42(d) | entri3 9381 |
| [Mendelson] p. 281 | Definition | df-r1 8627 |
| [Mendelson] p. 281 | Proposition 4.45 (b) to (a) | unir1 8676 |
| [Mendelson] p. 287 | Axiom system MK | ru 3434 |
| [MertziosUnger] p. 152 | Definition | df-frgr 27121 |
| [MertziosUnger] p. 153 | Remark 1 | frgrconngr 27158 |
| [MertziosUnger] p. 153 | Remark 2 | vdgn1frgrv2 27160 vdgn1frgrv3 27161 |
| [MertziosUnger] p. 153 | Remark 3 | vdgfrgrgt2 27162 |
| [MertziosUnger] p. 153 | Proposition 1(a) | n4cyclfrgr 27155 |
| [MertziosUnger] p. 153 | Proposition 1(b) | 2pthfrgr 27148 2pthfrgrrn 27146 2pthfrgrrn2 27147 |
| [Mittelstaedt] p. 9 | Definition | df-oc 28109 |
| [Monk1] p. 22 | Remark | conventions 27258 |
| [Monk1] p. 22 | Theorem 3.1 | conventions 27258 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3835 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 5207 ssrelf 29425 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 5209 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4713 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5651 coi2 5652 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 5339 rn0 5377 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5537 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 5227 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxp 5344 rnxp 5564 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 5199 xp0 5552 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5481 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5478 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 7104 imaexg 7103 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5477 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 6351 funfvop 6329 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 6239 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 6248 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5932 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 6512 dff13f 6513 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 6482 funrnex 7133 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 6505 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5619 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 4493 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 7185 df-1st 7168 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 7186 df-2nd 7169 |
| [Monk1] p. 112 | Theorem 15.17(v) | ranksn 8717 ranksnb 8690 |
| [Monk1] p. 112 | Theorem 15.17(iv) | rankuni2 8718 |
| [Monk1] p. 112 | Theorem 15.17(iii) | rankun 8719 rankunb 8713 |
| [Monk1] p. 113 | Theorem 15.18 | r1val3 8701 |
| [Monk1] p. 113 | Definition 15.19 | df-r1 8627 r1val2 8700 |
| [Monk1] p. 117 | Lemma | zorn2 9328 zorn2g 9325 |
| [Monk1] p. 133 | Theorem 18.11 | cardom 8812 |
| [Monk1] p. 133 | Theorem 18.12 | canth3 9383 |
| [Monk1] p. 133 | Theorem 18.14 | carduni 8807 |
| [Monk2] p. 105 | Axiom C4 | ax-4 1737 |
| [Monk2] p. 105 | Axiom C7 | ax-7 1935 |
| [Monk2] p. 105 | Axiom C8 | ax-12 2047 ax-c15 34174 ax12v2 2049 |
| [Monk2] p. 108 | Lemma 5 | ax-c4 34169 |
| [Monk2] p. 109 | Lemma 12 | ax-11 2034 |
| [Monk2] p. 109 | Lemma 15 | equvini 2346 equvinv 1959 eqvinop 4955 |
| [Monk2] p. 113 | Axiom C5-1 | ax-5 1839 ax5ALT 34192 |
| [Monk2] p. 113 | Axiom C5-2 | ax-10 2019 |
| [Monk2] p. 113 | Axiom C5-3 | ax-11 2034 |
| [Monk2] p. 114 | Lemma 21 | sp 2053 |
| [Monk2] p. 114 | Lemma 22 | axc4 2130 hba1-o 34182 hba1 2151 |
| [Monk2] p. 114 | Lemma 23 | nfia1 2030 |
| [Monk2] p. 114 | Lemma 24 | nfa2 2040 nfra2 2946 |
| [Moore] p. 53 | Part I | df-mre 16246 |
| [Munkres] p. 77 | Example 2 | distop 20799 indistop 20806 indistopon 20805 |
| [Munkres] p. 77 | Example 3 | fctop 20808 fctop2 20809 |
| [Munkres] p. 77 | Example 4 | cctop 20810 |
| [Munkres] p. 78 | Definition of basis | df-bases 20750 isbasis3g 20753 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 16104 tgval2 20760 |
| [Munkres] p. 79 | Remark | tgcl 20773 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 20767 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 20791 tgss3 20790 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 20792 basgen2 20793 |
| [Munkres] p. 83 | Exercise 3 | topdifinf 33197 topdifinfeq 33198 topdifinffin 33196 topdifinfindis 33194 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 20964 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 20842 topcld 20839 |
| [Munkres] p. 93 | Theorem 6.1(2) | iincld 20843 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 20845 |
| [Munkres] p. 94 | Definition of closure | clsval 20841 |
| [Munkres] p. 94 | Definition of interior | ntrval 20840 |
| [Munkres] p. 95 | Theorem 6.5(a) | clsndisj 20879 elcls 20877 |
| [Munkres] p. 95 | Theorem 6.5(b) | elcls3 20887 |
| [Munkres] p. 97 | Theorem 6.6 | clslp 20952 neindisj 20921 |
| [Munkres] p. 97 | Corollary 6.7 | cldlp 20954 |
| [Munkres] p. 97 | Definition of limit point | islp2 20949 lpval 20943 |
| [Munkres] p. 98 | Definition of Hausdorff space | df-haus 21119 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 21031 iscn 21039 iscn2 21042 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 21084 cncnp2 21085 cncnpi 21082 df-cnp 21032 iscnp 21041 iscnp2 21043 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 22348 |
| [Munkres] p. 128 | Theorem 10.3 | metcn4 23109 |
| [Nathanson] p. 123 | Remark | reprgt 30699 reprinfz1 30700 reprlt 30697 |
| [Nathanson] p. 123 | Definition | df-repr 30687 |
| [Nathanson] p. 123 | Chapter 5.1 | circlemethnat 30719 |
| [Nathanson] p. 123 | Proposition | breprexp 30711 breprexpnat 30712 itgexpif 30684 |
| [NielsenChuang] p. 195 | Equation 4.73 | unierri 28963 |
| [OeSilva] p. 2042 | Section 2 | ax-bgbltosilva 41698 |
| [Pfenning] p. 17 | Definition XM | natded 27260 |
| [Pfenning] p. 17 | Definition NNC | natded 27260 notnotrd 128 |
| [Pfenning] p. 17 | Definition ` `C | natded 27260 |
| [Pfenning] p. 18 | Rule" | natded 27260 |
| [Pfenning] p. 18 | Definition /\I | natded 27260 |
| [Pfenning] p. 18 | Definition ` `E | natded 27260 natded 27260 natded 27260 natded 27260 natded 27260 |
| [Pfenning] p. 18 | Definition ` `I | natded 27260 natded 27260 natded 27260 natded 27260 natded 27260 |
| [Pfenning] p. 18 | Definition ` `EL | natded 27260 |
| [Pfenning] p. 18 | Definition ` `ER | natded 27260 |
| [Pfenning] p. 18 | Definition ` `Ea,u | natded 27260 |
| [Pfenning] p. 18 | Definition ` `IR | natded 27260 |
| [Pfenning] p. 18 | Definition ` `Ia | natded 27260 |
| [Pfenning] p. 127 | Definition =E | natded 27260 |
| [Pfenning] p. 127 | Definition =I | natded 27260 |
| [Ponnusamy] p. 361 | Theorem 6.44 | cphip0l 23002 df-dip 27556 dip0l 27573 ip0l 19981 |
| [Ponnusamy] p. 361 | Equation 6.45 | cphipval 23042 ipval 27558 |
| [Ponnusamy] p. 362 | Equation I1 | dipcj 27569 ipcj 19979 |
| [Ponnusamy] p. 362 | Equation I3 | cphdir 23005 dipdir 27697 ipdir 19984 ipdiri 27685 |
| [Ponnusamy] p. 362 | Equation I4 | ipidsq 27565 nmsq 22994 |
| [Ponnusamy] p. 362 | Equation 6.46 | ip0i 27680 |
| [Ponnusamy] p. 362 | Equation 6.47 | ip1i 27682 |
| [Ponnusamy] p. 362 | Equation 6.48 | ip2i 27683 |
| [Ponnusamy] p. 363 | Equation I2 | cphass 23011 dipass 27700 ipass 19990 ipassi 27696 |
| [Prugovecki] p. 186 | Definition of bra | braval 28803 df-bra 28709 |
| [Prugovecki] p. 376 | Equation 8.1 | df-kb 28710 kbval 28813 |
| [PtakPulmannova] p. 66 | Proposition 3.2.17 | atomli 29241 |
| [PtakPulmannova] p. 68 | Lemma 3.1.4 | df-pclN 35174 |
| [PtakPulmannova] p. 68 | Lemma 3.2.20 | atcvat3i 29255 atcvat4i 29256 cvrat3 34728 cvrat4 34729 lsatcvat3 34339 |
| [PtakPulmannova] p. 68 | Definition 3.2.18 | cvbr 29141 cvrval 34556 df-cv 29138 df-lcv 34306 lspsncv0 19146 |
| [PtakPulmannova] p. 72 | Lemma 3.3.6 | pclfinN 35186 |
| [PtakPulmannova] p. 74 | Lemma 3.3.10 | pclcmpatN 35187 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2609 rabid 3116 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2455 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2615 |
| [Quine] p. 19 | Definition 2.9 | conventions 27258 df-v 3202 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2732 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2744 abid2f 2791 |
| [Quine] p. 40 | Theorem 6.1 | sb5 2430 |
| [Quine] p. 40 | Theorem 6.2 | sb56 2150 sb6 2429 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2618 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2622 eqid1 27323 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2629 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3436 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3437 dfsbcq2 3438 |
| [Quine] p. 43 | Theorem 6.8 | vex 3203 |
| [Quine] p. 43 | Theorem 6.9 | isset 3207 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 3288 spcgv 3293 spcimgf 3286 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3448 spsbcd 3449 |
| [Quine] p. 44 | Theorem 6.12 | elex 3212 |
| [Quine] p. 44 | Theorem 6.13 | elab 3350 elabg 3351 elabgf 3348 |
| [Quine] p. 44 | Theorem 6.14 | noel 3919 |
| [Quine] p. 48 | Theorem 7.2 | snprc 4253 |
| [Quine] p. 48 | Definition 7.1 | df-pr 4180 df-sn 4178 |
| [Quine] p. 49 | Theorem 7.4 | snss 4316 snssg 4327 |
| [Quine] p. 49 | Theorem 7.5 | prss 4351 prssg 4350 |
| [Quine] p. 49 | Theorem 7.6 | prid1 4297 prid1g 4295 prid2 4298 prid2g 4296 snid 4208 snidg 4206 |
| [Quine] p. 51 | Theorem 7.12 | snex 4908 |
| [Quine] p. 51 | Theorem 7.13 | prex 4909 |
| [Quine] p. 53 | Theorem 8.2 | unisn 4451 unisnALT 39162 unisng 4452 |
| [Quine] p. 53 | Theorem 8.3 | uniun 4456 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 4467 |
| [Quine] p. 54 | Theorem 8.7 | uni0 4465 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5861 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5852 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5862 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5866 |
| [Quine] p. 58 | Theorem 8.23 | iotaex 5868 |
| [Quine] p. 58 | Definition 9.1 | df-op 4184 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4982 opelopab 4997 opelopaba 4991 opelopabaf 4999 opelopabf 5000 opelopabg 4993 opelopabga 4988 opelopabgf 4995 oprabid 6677 |
| [Quine] p. 64 | Definition 9.11 | df-xp 5120 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 5122 |
| [Quine] p. 64 | Definition 9.15 | df-id 5024 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5954 |
| [Quine] p. 65 | Theorem 10.4 | funi 5920 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5939 funsng 5937 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5890 |
| [Quine] p. 65 | Definition 10.2 | args 5493 dffv4 6188 |
| [Quine] p. 68 | Definition 10.11 | conventions 27258 df-fv 5896 fv2 6186 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 13059 nn0opth2i 13058 nn0opthi 13057 omopthi 7737 |
| [Quine] p. 177 | Definition 25.2 | df-rdg 7506 |
| [Quine] p. 232 | Equation i | carddom 9376 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5976 funimaexg 5975 |
| [Quine] p. 331 | Axiom system NF | ru 3434 |
| [ReedSimon] p. 36 | Definition (iii) | ax-his3 27941 |
| [ReedSimon] p. 63 | Exercise 4(a) | df-dip 27556 polid 28016 polid2i 28014 polidi 28015 |
| [ReedSimon] p. 63 | Exercise 4(b) | df-ph 27668 |
| [ReedSimon] p. 195 | Remark | lnophm 28878 lnophmi 28877 |
| [Retherford] p. 49 | Exercise 1(i) | leopadd 28991 |
| [Retherford] p. 49 | Exercise 1(ii) | leopmul 28993 leopmuli 28992 |
| [Retherford] p. 49 | Exercise 1(iv) | leoptr 28996 |
| [Retherford] p. 49 | Definition VI.1 | df-leop 28711 leoppos 28985 |
| [Retherford] p. 49 | Exercise 1(iii) | leoptri 28995 |
| [Retherford] p. 49 | Definition of operator ordering | leop3 28984 |
| [Roman] p. 4 | Definition | df-dmat 20296 df-dmatalt 42187 |
| [Roman] p. 18 | Part Preliminaries | df-rng0 41875 |
| [Roman] p. 19 | Part Preliminaries | df-ring 18549 |
| [Roman] p. 46 | Theorem 1.6 | isldepslvec2 42274 |
| [Roman] p. 112 | Note | isldepslvec2 42274 ldepsnlinc 42297 zlmodzxznm 42286 |
| [Roman] p. 112 | Example | zlmodzxzequa 42285 zlmodzxzequap 42288 zlmodzxzldep 42293 |
| [Roman] p. 170 | Theorem 7.8 | cayleyhamilton 20695 |
| [Rosenlicht] p. 80 | Theorem | heicant 33444 |
| [Rosser] p. 281 | Definition | df-op 4184 |
| [RosserSchoenfeld] p. 71 | Theorem 12. | ax-ros335 30723 |
| [RosserSchoenfeld] p. 71 | Theorem 13. | ax-ros336 30724 |
| [Rotman] p. 28 | Remark | pgrpgt2nabl 42147 pmtr3ncom 17895 |
| [Rotman] p. 31 | Theorem 3.4 | symggen2 17891 |
| [Rotman] p. 42 | Theorem 3.15 | cayley 17834 cayleyth 17835 |
| [Rudin] p. 164 | Equation 27 | efcan 14826 |
| [Rudin] p. 164 | Equation 30 | efzval 14832 |
| [Rudin] p. 167 | Equation 48 | absefi 14926 |
| [Sanford] p. 39 | Remark | ax-mp 5 mto 188 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1696 |
| [Sanford] p. 39 | Rule 4 | mptxor 1694 |
| [Sanford] p. 40 | Rule 1 | mptnan 1693 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5511 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5514 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5510 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5508 |
| [Schechter] p. 78 | Definition of Moore collection of sets | df-mre 16246 |
| [Schechter] p. 79 | Definition of Moore closure | df-mrc 16247 |
| [Schechter] p. 82 | Section 4.5 | df-mrc 16247 |
| [Schechter] p. 84 | Definition (A) of an algebraic closure system | df-acs 16249 |
| [Schechter] p. 139 | Definition AC3 | dfac9 8958 |
| [Schechter] p. 141 | Definition (MC) | dfac11 37632 |
| [Schechter] p. 149 | Axiom DC1 | ax-dc 9268 axdc3 9276 |
| [Schechter] p. 187 | Definition of ring with unit | isring 18551 isrngo 33696 |
| [Schechter] p. 276 | Remark 11.6.e | span0 28401 |
| [Schechter] p. 276 | Definition of span | df-span 28168 spanval 28192 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 20797 |
| [Schwabhauser] p. 10 | Axiom A1 | axcgrrflx 25794 axtgcgrrflx 25361 |
| [Schwabhauser] p. 10 | Axiom A2 | axcgrtr 25795 |
| [Schwabhauser] p. 10 | Axiom A3 | axcgrid 25796 axtgcgrid 25362 |
| [Schwabhauser] p. 10 | Axioms A1 to A3 | df-trkgc 25347 |
| [Schwabhauser] p. 11 | Axiom A4 | axsegcon 25807 axtgsegcon 25363 df-trkgcb 25349 |
| [Schwabhauser] p. 11 | Axiom A5 | ax5seg 25818 axtg5seg 25364 df-trkgcb 25349 |
| [Schwabhauser] p. 11 | Axiom A6 | axbtwnid 25819 axtgbtwnid 25365 df-trkgb 25348 |
| [Schwabhauser] p. 12 | Axiom A7 | axpasch 25821 axtgpasch 25366 df-trkgb 25348 |
| [Schwabhauser] p. 12 | Axiom A8 | axlowdim2 25840 df-trkg2d 30743 |
| [Schwabhauser] p. 13 | Axiom A8 | axtglowdim2 25369 |
| [Schwabhauser] p. 13 | Axiom A9 | axtgupdim2 25370 df-trkg2d 30743 |
| [Schwabhauser] p. 13 | Axiom A10 | axeuclid 25843 axtgeucl 25371 df-trkge 25350 |
| [Schwabhauser] p. 13 | Axiom A11 | axcont 25856 axtgcont 25368 axtgcont1 25367 df-trkgb 25348 |
| [Schwabhauser] p. 27 | Theorem 2.1 | cgrrflx 32094 |
| [Schwabhauser] p. 27 | Theorem 2.2 | cgrcomim 32096 |
| [Schwabhauser] p. 27 | Theorem 2.3 | cgrtr 32099 |
| [Schwabhauser] p. 27 | Theorem 2.4 | cgrcoml 32103 |
| [Schwabhauser] p. 27 | Theorem 2.5 | cgrcomr 32104 tgcgrcomimp 25372 tgcgrcoml 25374 tgcgrcomr 25373 |
| [Schwabhauser] p. 28 | Theorem 2.8 | cgrtriv 32109 tgcgrtriv 25379 |
| [Schwabhauser] p. 28 | Theorem 2.10 | 5segofs 32113 tg5segofs 30751 |
| [Schwabhauser] p. 28 | Definition 2.10 | df-afs 30748 df-ofs 32090 |
| [Schwabhauser] p. 29 | Theorem 2.11 | cgrextend 32115 tgcgrextend 25380 |
| [Schwabhauser] p. 29 | Theorem 2.12 | segconeq 32117 tgsegconeq 25381 |
| [Schwabhauser] p. 30 | Theorem 3.1 | btwnouttr2 32129 btwntriv2 32119 tgbtwntriv2 25382 |
| [Schwabhauser] p. 30 | Theorem 3.2 | btwncomim 32120 tgbtwncom 25383 |
| [Schwabhauser] p. 30 | Theorem 3.3 | btwntriv1 32123 tgbtwntriv1 25386 |
| [Schwabhauser] p. 30 | Theorem 3.4 | btwnswapid 32124 tgbtwnswapid 25387 |
| [Schwabhauser] p. 30 | Theorem 3.5 | btwnexch2 32130 btwnintr 32126 tgbtwnexch2 25391 tgbtwnintr 25388 |
| [Schwabhauser] p. 30 | Theorem 3.6 | btwnexch 32132 btwnexch3 32127 tgbtwnexch 25393 tgbtwnexch3 25389 |
| [Schwabhauser] p. 30 | Theorem 3.7 | btwnouttr 32131 tgbtwnouttr 25392 tgbtwnouttr2 25390 |
| [Schwabhauser] p. 32 | Theorem 3.13 | axlowdim1 25839 |
| [Schwabhauser] p. 32 | Theorem 3.14 | btwndiff 32134 tgbtwndiff 25401 |
| [Schwabhauser] p. 33 | Theorem 3.17 | tgtrisegint 25394 trisegint 32135 |
| [Schwabhauser] p. 34 | Theorem 4.2 | ifscgr 32151 tgifscgr 25403 |
| [Schwabhauser] p. 34 | Theorem 4.11 | colcom 25453 colrot1 25454 colrot2 25455 lncom 25517 lnrot1 25518 lnrot2 25519 |
| [Schwabhauser] p. 34 | Definition 4.1 | df-ifs 32147 |
| [Schwabhauser] p. 35 | Theorem 4.3 | cgrsub 32152 tgcgrsub 25404 |
| [Schwabhauser] p. 35 | Theorem 4.5 | cgrxfr 32162 tgcgrxfr 25413 |
| [Schwabhauser] p. 35 | Statement 4.4 | ercgrg 25412 |
| [Schwabhauser] p. 35 | Definition 4.4 | df-cgr3 32148 df-cgrg 25406 |
| [Schwabhauser] p. 36 | Theorem 4.6 | btwnxfr 32163 tgbtwnxfr 25425 |
| [Schwabhauser] p. 36 | Theorem 4.11 | colinearperm1 32169 colinearperm2 32171 colinearperm3 32170 colinearperm4 32172 colinearperm5 32173 |
| [Schwabhauser] p. 36 | Definition 4.8 | df-ismt 25428 |
| [Schwabhauser] p. 36 | Definition 4.10 | df-colinear 32146 tgellng 25448 tglng 25441 |
| [Schwabhauser] p. 37 | Theorem 4.12 | colineartriv1 32174 |
| [Schwabhauser] p. 37 | Theorem 4.13 | colinearxfr 32182 lnxfr 25461 |
| [Schwabhauser] p. 37 | Theorem 4.14 | lineext 32183 lnext 25462 |
| [Schwabhauser] p. 37 | Theorem 4.16 | fscgr 32187 tgfscgr 25463 |
| [Schwabhauser] p. 37 | Theorem 4.17 | linecgr 32188 lncgr 25464 |
| [Schwabhauser] p. 37 | Definition 4.15 | df-fs 32149 |
| [Schwabhauser] p. 38 | Theorem 4.18 | lineid 32190 lnid 25465 |
| [Schwabhauser] p. 38 | Theorem 4.19 | idinside 32191 tgidinside 25466 |
| [Schwabhauser] p. 39 | Theorem 5.1 | btwnconn1 32208 tgbtwnconn1 25470 |
| [Schwabhauser] p. 41 | Theorem 5.2 | btwnconn2 32209 tgbtwnconn2 25471 |
| [Schwabhauser] p. 41 | Theorem 5.3 | btwnconn3 32210 tgbtwnconn3 25472 |
| [Schwabhauser] p. 41 | Theorem 5.5 | brsegle2 32216 |
| [Schwabhauser] p. 41 | Definition 5.4 | df-segle 32214 legov 25480 |
| [Schwabhauser] p. 41 | Definition 5.5 | legov2 25481 |
| [Schwabhauser] p. 42 | Remark 5.13 | legso 25494 |
| [Schwabhauser] p. 42 | Theorem 5.6 | seglecgr12im 32217 |
| [Schwabhauser] p. 42 | Theorem 5.7 | seglerflx 32219 |
| [Schwabhauser] p. 42 | Theorem 5.8 | segletr 32221 |
| [Schwabhauser] p. 42 | Theorem 5.9 | segleantisym 32222 |
| [Schwabhauser] p. 42 | Theorem 5.10 | seglelin 32223 |
| [Schwabhauser] p. 42 | Theorem 5.11 | seglemin 32220 |
| [Schwabhauser] p. 42 | Theorem 5.12 | colinbtwnle 32225 |
| [Schwabhauser] p. 42 | Proposition 5.7 | legid 25482 |
| [Schwabhauser] p. 42 | Proposition 5.8 | legtrd 25484 |
| [Schwabhauser] p. 42 | Proposition 5.9 | legtri3 25485 |
| [Schwabhauser] p. 42 | Proposition 5.10 | legtrid 25486 |
| [Schwabhauser] p. 42 | Proposition 5.11 | leg0 25487 |
| [Schwabhauser] p. 43 | Theorem 6.2 | btwnoutside 32232 |
| [Schwabhauser] p. 43 | Theorem 6.3 | broutsideof3 32233 |
| [Schwabhauser] p. 43 | Theorem 6.4 | broutsideof 32228 df-outsideof 32227 |
| [Schwabhauser] p. 43 | Definition 6.1 | broutsideof2 32229 ishlg 25497 |
| [Schwabhauser] p. 44 | Theorem 6.4 | hlln 25502 |
| [Schwabhauser] p. 44 | Theorem 6.5 | hlid 25504 outsideofrflx 32234 |
| [Schwabhauser] p. 44 | Theorem 6.6 | hlcomb 25498 hlcomd 25499 outsideofcom 32235 |
| [Schwabhauser] p. 44 | Theorem 6.7 | hltr 25505 outsideoftr 32236 |
| [Schwabhauser] p. 44 | Theorem 6.11 | hlcgreu 25513 outsideofeu 32238 |
| [Schwabhauser] p. 44 | Definition 6.8 | df-ray 32245 |
| [Schwabhauser] p. 45 | Part 2 | df-lines2 32246 |
| [Schwabhauser] p. 45 | Theorem 6.13 | outsidele 32239 |
| [Schwabhauser] p. 45 | Theorem 6.15 | lineunray 32254 |
| [Schwabhauser] p. 45 | Theorem 6.16 | lineelsb2 32255 tglineelsb2 25527 |
| [Schwabhauser] p. 45 | Theorem 6.17 | linecom 32257 linerflx1 32256 linerflx2 32258 tglinecom 25530 tglinerflx1 25528 tglinerflx2 25529 |
| [Schwabhauser] p. 45 | Theorem 6.18 | linethru 32260 tglinethru 25531 |
| [Schwabhauser] p. 45 | Definition 6.14 | df-line2 32244 tglng 25441 |
| [Schwabhauser] p. 45 | Proposition 6.13 | legbtwn 25489 |
| [Schwabhauser] p. 46 | Theorem 6.19 | linethrueu 32263 tglinethrueu 25534 |
| [Schwabhauser] p. 46 | Theorem 6.21 | lineintmo 32264 tglineineq 25538 tglineinteq 25540 tglineintmo 25537 |
| [Schwabhauser] p. 46 | Theorem 6.23 | colline 25544 |
| [Schwabhauser] p. 46 | Theorem 6.24 | tglowdim2l 25545 |
| [Schwabhauser] p. 46 | Theorem 6.25 | tglowdim2ln 25546 |
| [Schwabhauser] p. 49 | Theorem 7.3 | mirinv 25561 |
| [Schwabhauser] p. 49 | Theorem 7.7 | mirmir 25557 |
| [Schwabhauser] p. 49 | Theorem 7.8 | mirreu3 25549 |
| [Schwabhauser] p. 49 | Definition 7.5 | df-mir 25548 ismir 25554 mirbtwn 25553 mircgr 25552 mirfv 25551 mirval 25550 |
| [Schwabhauser] p. 50 | Theorem 7.8 | mirreu 25559 |
| [Schwabhauser] p. 50 | Theorem 7.9 | mireq 25560 |
| [Schwabhauser] p. 50 | Theorem 7.10 | mirinv 25561 |
| [Schwabhauser] p. 50 | Theorem 7.11 | mirf1o 25564 |
| [Schwabhauser] p. 50 | Theorem 7.13 | miriso 25565 |
| [Schwabhauser] p. 51 | Theorem 7.14 | mirmot 25570 |
| [Schwabhauser] p. 51 | Theorem 7.15 | mirbtwnb 25567 mirbtwni 25566 |
| [Schwabhauser] p. 51 | Theorem 7.16 | mircgrs 25568 |
| [Schwabhauser] p. 51 | Theorem 7.17 | miduniq 25580 |
| [Schwabhauser] p. 52 | Lemma 7.21 | symquadlem 25584 |
| [Schwabhauser] p. 52 | Theorem 7.18 | miduniq1 25581 |
| [Schwabhauser] p. 52 | Theorem 7.19 | miduniq2 25582 |
| [Schwabhauser] p. 52 | Theorem 7.20 | colmid 25583 |
| [Schwabhauser] p. 53 | Lemma 7.22 | krippen 25586 |
| [Schwabhauser] p. 55 | Lemma 7.25 | midexlem 25587 |
| [Schwabhauser] p. 57 | Theorem 8.2 | ragcom 25593 |
| [Schwabhauser] p. 57 | Definition 8.1 | df-rag 25589 israg 25592 |
| [Schwabhauser] p. 58 | Theorem 8.3 | ragcol 25594 |
| [Schwabhauser] p. 58 | Theorem 8.4 | ragmir 25595 |
| [Schwabhauser] p. 58 | Theorem 8.5 | ragtrivb 25597 |
| [Schwabhauser] p. 58 | Theorem 8.6 | ragflat2 25598 |
| [Schwabhauser] p. 58 | Theorem 8.7 | ragflat 25599 |
| [Schwabhauser] p. 58 | Theorem 8.8 | ragtriva 25600 |
| [Schwabhauser] p. 58 | Theorem 8.9 | ragflat3 25601 ragncol 25604 |
| [Schwabhauser] p. 58 | Theorem 8.10 | ragcgr 25602 |
| [Schwabhauser] p. 59 | Theorem 8.12 | perpcom 25608 |
| [Schwabhauser] p. 59 | Theorem 8.13 | ragperp 25612 |
| [Schwabhauser] p. 59 | Theorem 8.14 | perpneq 25609 |
| [Schwabhauser] p. 59 | Definition 8.11 | df-perpg 25591 isperp 25607 |
| [Schwabhauser] p. 59 | Definition 8.13 | isperp2 25610 |
| [Schwabhauser] p. 60 | Theorem 8.18 | foot 25614 |
| [Schwabhauser] p. 62 | Lemma 8.20 | colperpexlem1 25622 colperpexlem2 25623 |
| [Schwabhauser] p. 63 | Theorem 8.21 | colperpex 25625 colperpexlem3 25624 |
| [Schwabhauser] p. 64 | Theorem 8.22 | mideu 25630 midex 25629 |
| [Schwabhauser] p. 66 | Lemma 8.24 | opphllem 25627 |
| [Schwabhauser] p. 67 | Theorem 9.2 | oppcom 25636 |
| [Schwabhauser] p. 67 | Definition 9.1 | islnopp 25631 |
| [Schwabhauser] p. 68 | Lemma 9.3 | opphllem2 25640 |
| [Schwabhauser] p. 68 | Lemma 9.4 | opphllem5 25643 opphllem6 25644 |
| [Schwabhauser] p. 69 | Theorem 9.5 | opphl 25646 |
| [Schwabhauser] p. 69 | Theorem 9.6 | axtgpasch 25366 |
| [Schwabhauser] p. 70 | Theorem 9.6 | outpasch 25647 |
| [Schwabhauser] p. 71 | Theorem 9.8 | lnopp2hpgb 25655 |
| [Schwabhauser] p. 71 | Definition 9.7 | df-hpg 25650 hpgbr 25652 |
| [Schwabhauser] p. 72 | Lemma 9.10 | hpgerlem 25657 |
| [Schwabhauser] p. 72 | Theorem 9.9 | lnoppnhpg 25656 |
| [Schwabhauser] p. 72 | Theorem 9.11 | hpgid 25658 |
| [Schwabhauser] p. 72 | Theorem 9.12 | hpgcom 25659 |
| [Schwabhauser] p. 72 | Theorem 9.13 | hpgtr 25660 |
| [Schwabhauser] p. 73 | Theorem 9.18 | colopp 25661 |
| [Schwabhauser] p. 73 | Theorem 9.19 | colhp 25662 |
| [Schwabhauser] p. 88 | Theorem 10.2 | lmieu 25676 |
| [Schwabhauser] p. 88 | Definition 10.1 | df-mid 25666 |
| [Schwabhauser] p. 89 | Theorem 10.4 | lmicom 25680 |
| [Schwabhauser] p. 89 | Theorem 10.5 | lmilmi 25681 |
| [Schwabhauser] p. 89 | Theorem 10.6 | lmireu 25682 |
| [Schwabhauser] p. 89 | Theorem 10.7 | lmieq 25683 |
| [Schwabhauser] p. 89 | Theorem 10.8 | lmiinv 25684 |
| [Schwabhauser] p. 89 | Theorem 10.9 | lmif1o 25687 |
| [Schwabhauser] p. 89 | Theorem 10.10 | lmiiso 25689 |
| [Schwabhauser] p. 89 | Definition 10.3 | df-lmi 25667 |
| [Schwabhauser] p. 90 | Theorem 10.11 | lmimot 25690 |
| [Schwabhauser] p. 91 | Theorem 10.12 | hypcgr 25693 |
| [Schwabhauser] p. 92 | Theorem 10.14 | lmiopp 25694 |
| [Schwabhauser] p. 92 | Theorem 10.15 | lnperpex 25695 |
| [Schwabhauser] p. 92 | Theorem 10.16 | trgcopy 25696 trgcopyeu 25698 |
| [Schwabhauser] p. 95 | Definition 11.2 | dfcgra2 25721 |
| [Schwabhauser] p. 95 | Definition 11.3 | iscgra 25701 |
| [Schwabhauser] p. 95 | Proposition 11.4 | cgracgr 25710 |
| [Schwabhauser] p. 95 | Proposition 11.10 | cgrahl1 25708 cgrahl2 25709 |
| [Schwabhauser] p. 96 | Theorem 11.6 | cgraid 25711 |
| [Schwabhauser] p. 96 | Theorem 11.9 | cgraswap 25712 |
| [Schwabhauser] p. 97 | Theorem 11.7 | cgracom 25714 |
| [Schwabhauser] p. 97 | Theorem 11.8 | cgratr 25715 |
| [Schwabhauser] p. 97 | Theorem 11.21 | cgrabtwn 25717 cgrahl 25718 |
| [Schwabhauser] p. 98 | Theorem 11.13 | sacgr 25722 |
| [Schwabhauser] p. 98 | Theorem 11.14 | oacgr 25723 |
| [Schwabhauser] p. 98 | Theorem 11.15 | acopy 25724 acopyeu 25725 |
| [Schwabhauser] p. 101 | Theorem 11.24 | inagswap 25730 |
| [Schwabhauser] p. 101 | Theorem 11.25 | inaghl 25731 |
| [Schwabhauser] p. 101 | Property for point ` ` to lie in the angle ` ` Defnition 11.23 | isinag 25729 |
| [Schwabhauser] p. 102 | Lemma 11.28 | cgrg3col4 25734 |
| [Schwabhauser] p. 102 | Definition 11.27 | df-leag 25732 isleag 25733 |
| [Schwabhauser] p. 107 | Theorem 11.49 | tgsas 25736 tgsas1 25735 tgsas2 25737 tgsas3 25738 |
| [Schwabhauser] p. 108 | Theorem 11.50 | tgasa 25740 tgasa1 25739 |
| [Schwabhauser] p. 109 | Theorem 11.51 | tgsss1 25741 tgsss2 25742 tgsss3 25743 |
| [Shapiro] p. 230 | Theorem 6.5.1 | dchrhash 24996 dchrsum 24994 dchrsum2 24993 sumdchr 24997 |
| [Shapiro] p. 232 | Theorem 6.5.2 | dchr2sum 24998 sum2dchr 24999 |
| [Shapiro], p. 199 | Lemma 6.1C.2 | ablfacrp 18465 ablfacrp2 18466 |
| [Shapiro], p. 328 | Equation 9.2.4 | vmasum 24941 |
| [Shapiro], p. 329 | Equation 9.2.7 | logfac2 24942 |
| [Shapiro], p. 329 | Equation 9.2.9 | logfacrlim 24949 |
| [Shapiro], p. 331 | Equation 9.2.13 | vmadivsum 25171 |
| [Shapiro], p. 331 | Equation 9.2.14 | rplogsumlem2 25174 |
| [Shapiro], p. 336 | Exercise 9.1.7 | vmalogdivsum 25228 vmalogdivsum2 25227 |
| [Shapiro], p. 375 | Theorem 9.4.1 | dirith 25218 dirith2 25217 |
| [Shapiro], p. 375 | Equation 9.4.3 | rplogsum 25216 rpvmasum 25215 rpvmasum2 25201 |
| [Shapiro], p. 376 | Equation 9.4.7 | rpvmasumlem 25176 |
| [Shapiro], p. 376 | Equation 9.4.8 | dchrvmasum 25214 |
| [Shapiro], p. 377 | Lemma 9.4.1 | dchrisum 25181 dchrisumlem1 25178 dchrisumlem2 25179 dchrisumlem3 25180 dchrisumlema 25177 |
| [Shapiro], p. 377 | Equation 9.4.11 | dchrvmasumlem1 25184 |
| [Shapiro], p. 379 | Equation 9.4.16 | dchrmusum 25213 dchrmusumlem 25211 dchrvmasumlem 25212 |
| [Shapiro], p. 380 | Lemma 9.4.2 | dchrmusum2 25183 |
| [Shapiro], p. 380 | Lemma 9.4.3 | dchrvmasum2lem 25185 |
| [Shapiro], p. 382 | Lemma 9.4.4 | dchrisum0 25209 dchrisum0re 25202 dchrisumn0 25210 |
| [Shapiro], p. 382 | Equation 9.4.27 | dchrisum0fmul 25195 |
| [Shapiro], p. 382 | Equation 9.4.29 | dchrisum0flb 25199 |
| [Shapiro], p. 383 | Equation 9.4.30 | dchrisum0fno1 25200 |
| [Shapiro], p. 403 | Equation 10.1.16 | pntrsumbnd 25255 pntrsumbnd2 25256 pntrsumo1 25254 |
| [Shapiro], p. 405 | Equation 10.2.1 | mudivsum 25219 |
| [Shapiro], p. 406 | Equation 10.2.6 | mulogsum 25221 |
| [Shapiro], p. 407 | Equation 10.2.7 | mulog2sumlem1 25223 |
| [Shapiro], p. 407 | Equation 10.2.8 | mulog2sum 25226 |
| [Shapiro], p. 418 | Equation 10.4.6 | logsqvma 25231 |
| [Shapiro], p. 418 | Equation 10.4.8 | logsqvma2 25232 |
| [Shapiro], p. 419 | Equation 10.4.10 | selberg 25237 |
| [Shapiro], p. 420 | Equation 10.4.12 | selberg2lem 25239 |
| [Shapiro], p. 420 | Equation 10.4.14 | selberg2 25240 |
| [Shapiro], p. 422 | Equation 10.6.7 | selberg3 25248 |
| [Shapiro], p. 422 | Equation 10.4.20 | selberg4lem1 25249 |
| [Shapiro], p. 422 | Equation 10.4.21 | selberg3lem1 25246 selberg3lem2 25247 |
| [Shapiro], p. 422 | Equation 10.4.23 | selberg4 25250 |
| [Shapiro], p. 427 | Theorem 10.5.2 | chpdifbnd 25244 |
| [Shapiro], p. 428 | Equation 10.6.2 | selbergr 25257 |
| [Shapiro], p. 429 | Equation 10.6.8 | selberg3r 25258 |
| [Shapiro], p. 430 | Equation 10.6.11 | selberg4r 25259 |
| [Shapiro], p. 431 | Equation 10.6.15 | pntrlog2bnd 25273 |
| [Shapiro], p. 434 | Equation 10.6.27 | pntlema 25285 pntlemb 25286 pntlemc 25284 pntlemd 25283 pntlemg 25287 |
| [Shapiro], p. 435 | Equation 10.6.29 | pntlema 25285 |
| [Shapiro], p. 436 | Lemma 10.6.1 | pntpbnd 25277 |
| [Shapiro], p. 436 | Lemma 10.6.2 | pntibnd 25282 |
| [Shapiro], p. 436 | Equation 10.6.34 | pntlema 25285 |
| [Shapiro], p. 436 | Equation 10.6.35 | pntlem3 25298 pntleml 25300 |
| [Stoll] p. 13 | Definition corresponds to | dfsymdif3 3893 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3977 dif0 3950 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdir 4056 |
| [Stoll] p. 17 | Theorem 5.1(5) | unvdif 4042 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3885 |
| [Stoll] p. 19 | Theorem 5.2(13') | indm 3886 |
| [Stoll] p. 20 | Remark | invdif 3868 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 4186 |
| [Stoll] p. 43 | Definition | uniiun 4573 |
| [Stoll] p. 44 | Definition | intiin 4574 |
| [Stoll] p. 45 | Definition | df-iin 4523 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4522 |
| [Stoll] p. 176 | Theorem 3.4(27) | iman 440 |
| [Stoll] p. 262 | Example 4.1 | dfsymdif3 3893 |
| [Strang] p. 242 | Section 6.3 | expgrowth 38534 |
| [Suppes] p. 22 | Theorem 2 | eq0 3929 eq0f 3925 |
| [Suppes] p. 22 | Theorem 4 | eqss 3618 eqssd 3620 eqssi 3619 |
| [Suppes] p. 23 | Theorem 5 | ss0 3974 ss0b 3973 |
| [Suppes] p. 23 | Theorem 6 | sstr 3611 sstrALT2 39070 |
| [Suppes] p. 23 | Theorem 7 | pssirr 3707 |
| [Suppes] p. 23 | Theorem 8 | pssn2lp 3708 |
| [Suppes] p. 23 | Theorem 9 | psstr 3711 |
| [Suppes] p. 23 | Theorem 10 | pssss 3702 |
| [Suppes] p. 25 | Theorem 12 | elin 3796 elun 3753 |
| [Suppes] p. 26 | Theorem 15 | inidm 3822 |
| [Suppes] p. 26 | Theorem 16 | in0 3968 |
| [Suppes] p. 27 | Theorem 23 | unidm 3756 |
| [Suppes] p. 27 | Theorem 24 | un0 3967 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3776 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3783 |
| [Suppes] p. 27 | Theorem 27 | unss 3787 |
| [Suppes] p. 27 | Theorem 28 | indir 3875 |
| [Suppes] p. 27 | Theorem 29 | undir 3876 |
| [Suppes] p. 28 | Theorem 32 | difid 3948 |
| [Suppes] p. 29 | Theorem 33 | difin 3861 |
| [Suppes] p. 29 | Theorem 34 | indif 3869 |
| [Suppes] p. 29 | Theorem 35 | undif1 4043 |
| [Suppes] p. 29 | Theorem 36 | difun2 4048 |
| [Suppes] p. 29 | Theorem 37 | difin0 4041 |
| [Suppes] p. 29 | Theorem 38 | disjdif 4040 |
| [Suppes] p. 29 | Theorem 39 | difundi 3879 |
| [Suppes] p. 29 | Theorem 40 | difindi 3881 |
| [Suppes] p. 30 | Theorem 41 | nalset 4795 |
| [Suppes] p. 39 | Theorem 61 | uniss 4458 |
| [Suppes] p. 39 | Theorem 65 | uniop 4977 |
| [Suppes] p. 41 | Theorem 70 | intsn 4513 |
| [Suppes] p. 42 | Theorem 71 | intpr 4510 intprg 4511 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4940 |
| [Suppes] p. 42 | Theorem 78 | intun 4509 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4554 dfiun2g 4552 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4555 |
| [Suppes] p. 47 | Theorem 86 | elpw 4164 elpw2 4828 elpw2g 4827 elpwg 4166 elpwgdedVD 39153 |
| [Suppes] p. 47 | Theorem 87 | pwid 4174 |
| [Suppes] p. 47 | Theorem 89 | pw0 4343 |
| [Suppes] p. 48 | Theorem 90 | pwpw0 4344 |
| [Suppes] p. 52 | Theorem 101 | xpss12 5225 |
| [Suppes] p. 52 | Theorem 102 | xpindi 5255 xpindir 5256 |
| [Suppes] p. 52 | Theorem 103 | xpundi 5171 xpundir 5172 |
| [Suppes] p. 54 | Theorem 105 | elirrv 8504 |
| [Suppes] p. 58 | Theorem 2 | relss 5206 |
| [Suppes] p. 59 | Theorem 4 | eldm 5321 eldm2 5322 eldm2g 5320 eldmg 5319 |
| [Suppes] p. 59 | Definition 3 | df-dm 5124 |
| [Suppes] p. 60 | Theorem 6 | dmin 5332 |
| [Suppes] p. 60 | Theorem 8 | rnun 5541 |
| [Suppes] p. 60 | Theorem 9 | rnin 5542 |
| [Suppes] p. 60 | Definition 4 | dfrn2 5311 |
| [Suppes] p. 61 | Theorem 11 | brcnv 5305 brcnvg 5303 |
| [Suppes] p. 62 | Equation 5 | elcnv 5299 elcnv2 5300 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5503 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5540 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5538 |
| [Suppes] p. 63 | Theorem 20 | co02 5649 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5385 |
| [Suppes] p. 63 | Definition 7 | df-co 5123 |
| [Suppes] p. 64 | Theorem 26 | cnvco 5308 |
| [Suppes] p. 64 | Theorem 27 | coass 5654 |
| [Suppes] p. 65 | Theorem 31 | resundi 5410 |
| [Suppes] p. 65 | Theorem 34 | elima 5471 elima2 5472 elima3 5473 elimag 5470 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5545 |
| [Suppes] p. 66 | Theorem 40 | dminss 5547 |
| [Suppes] p. 66 | Theorem 41 | imainss 5548 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5551 |
| [Suppes] p. 81 | Definition 34 | dfec2 7745 |
| [Suppes] p. 82 | Theorem 72 | elec 7786 elecALTV 34030 elecg 7785 |
| [Suppes] p. 82 | Theorem 73 | erth 7791 erth2 7792 |
| [Suppes] p. 83 | Theorem 74 | erdisj 7794 |
| [Suppes] p. 89 | Theorem 96 | map0b 7896 |
| [Suppes] p. 89 | Theorem 97 | map0 7898 map0g 7897 |
| [Suppes] p. 89 | Theorem 98 | mapsn 7899 |
| [Suppes] p. 89 | Theorem 99 | mapss 7900 |
| [Suppes] p. 91 | Definition 12(ii) | alephsuc 8891 |
| [Suppes] p. 91 | Definition 12(iii) | alephlim 8890 |
| [Suppes] p. 92 | Theorem 1 | enref 7988 enrefg 7987 |
| [Suppes] p. 92 | Theorem 2 | ensym 8005 ensymb 8004 ensymi 8006 |
| [Suppes] p. 92 | Theorem 3 | entr 8008 |
| [Suppes] p. 92 | Theorem 4 | unen 8040 |
| [Suppes] p. 94 | Theorem 15 | endom 7982 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 8001 |
| [Suppes] p. 94 | Theorem 17 | domtr 8009 |
| [Suppes] p. 95 | Theorem 18 | sbth 8080 |
| [Suppes] p. 97 | Theorem 23 | canth2 8113 canth2g 8114 |
| [Suppes] p. 97 | Definition 3 | brsdom2 8084 df-sdom 7958 dfsdom2 8083 |
| [Suppes] p. 97 | Theorem 21(i) | sdomirr 8097 |
| [Suppes] p. 97 | Theorem 22(i) | domnsym 8086 |
| [Suppes] p. 97 | Theorem 21(ii) | sdomnsym 8085 |
| [Suppes] p. 97 | Theorem 22(ii) | domsdomtr 8095 |
| [Suppes] p. 97 | Theorem 22(iv) | brdom2 7985 |
| [Suppes] p. 97 | Theorem 21(iii) | sdomtr 8098 |
| [Suppes] p. 97 | Theorem 22(iii) | sdomdomtr 8093 |
| [Suppes] p. 98 | Exercise 4 | fundmen 8030 fundmeng 8031 |
| [Suppes] p. 98 | Exercise 6 | xpdom3 8058 |
| [Suppes] p. 98 | Exercise 11 | sdomentr 8094 |
| [Suppes] p. 104 | Theorem 37 | fofi 8252 |
| [Suppes] p. 104 | Theorem 38 | pwfi 8261 |
| [Suppes] p. 105 | Theorem 40 | pwfi 8261 |
| [Suppes] p. 111 | Axiom for cardinal numbers | carden 9373 |
| [Suppes] p. 130 | Definition 3 | df-tr 4753 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 6986 |
| [Suppes] p. 134 | Definition 6 | df-suc 5729 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 7096 finds 7092 finds1 7095 finds2 7094 |
| [Suppes] p. 151 | Theorem 42 | isfinite 8549 isfinite2 8218 isfiniteg 8220 unbnn 8216 |
| [Suppes] p. 162 | Definition 5 | df-ltnq 9740 df-ltpq 9732 |
| [Suppes] p. 197 | Theorem Schema 4 | tfindes 7062 tfinds 7059 tfinds2 7063 |
| [Suppes] p. 209 | Theorem 18 | oaord1 7631 |
| [Suppes] p. 209 | Theorem 21 | oaword2 7633 |
| [Suppes] p. 211 | Theorem 25 | oaass 7641 |
| [Suppes] p. 225 | Definition 8 | iscard2 8802 |
| [Suppes] p. 227 | Theorem 56 | ondomon 9385 |
| [Suppes] p. 228 | Theorem 59 | harcard 8804 |
| [Suppes] p. 228 | Definition 12(i) | aleph0 8889 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 5775 |
| [Suppes] p. 228 | Theorem Schema 62 | onminesb 6998 onminsb 6999 |
| [Suppes] p. 229 | Theorem 64 | alephval2 9394 |
| [Suppes] p. 229 | Theorem 65 | alephcard 8893 |
| [Suppes] p. 229 | Theorem 66 | alephord2i 8900 |
| [Suppes] p. 229 | Theorem 67 | alephnbtwn 8894 |
| [Suppes] p. 229 | Definition 12 | df-aleph 8766 |
| [Suppes] p. 242 | Theorem 6 | weth 9317 |
| [Suppes] p. 242 | Theorem 8 | entric 9379 |
| [Suppes] p. 242 | Theorem 9 | carden 9373 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2602 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2615 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2618 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2617 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2641 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6654 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3434 |
| [TakeutiZaring] p. 15 | Axiom 2 | zfpair 4904 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 4198 elpr2 4199 elprg 4196 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 4192 elsn2 4211 elsn2g 4210 elsng 4191 velsn 4193 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4935 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 4187 sneqr 4371 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 4195 dfsn2 4190 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 6953 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4945 |
| [TakeutiZaring] p. 16 | Exercise 7 | opex 4932 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4916 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 6956 unexg 6959 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 4231 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 4437 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3581 df-un 3579 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 4449 uniprg 4450 |
| [TakeutiZaring] p. 17 | Axiom 4 | pwex 4848 pwexg 4850 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 4230 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 5794 elsucg 5792 sstr2 3610 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3757 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3805 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3770 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3823 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3873 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3874 |
| [TakeutiZaring] p. 17 | Definition 5.9 | df-pss 3590 dfss2 3591 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 4160 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3784 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3588 sseqin2 3817 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3624 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3833 inss2 3834 |
| [TakeutiZaring] p. 18 | Exercise 13 | nss 3663 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 4444 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4917 sspwimp 39154 sspwimpALT 39161 sspwimpALT2 39164 sspwimpcf 39156 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4925 |
| [TakeutiZaring] p. 19 | Axiom 5 | ax-rep 4771 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2921 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4790 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3577 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3917 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3948 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0 3931 n0f 3927 neq0 3930 neq0f 3926 |
| [TakeutiZaring] p. 21 | Axiom 6 | zfreg 8500 |
| [TakeutiZaring] p. 21 | Axiom 6' | zfregs 8608 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 8610 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 3202 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4796 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3972 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4802 ssexg 4804 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4799 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 8507 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 8505 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0 3942 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3736 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3 3888 undif3VD 39118 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3737 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3744 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2917 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2918 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 6962 xpexg 6960 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 5121 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5960 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 6109 fun11 5963 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5900 svrelfun 5961 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 5310 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 5312 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 5126 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 5127 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 5123 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5589 dfrel2 5583 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 5226 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 5235 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 5241 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 5254 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5426 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5401 opelresALTV 34031 opelresg 5404 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5419 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5422 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5427 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5929 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5633 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5928 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 6110 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2509 |
| [TakeutiZaring] p. 26 | Definition 6.11 | conventions 27258 df-fv 5896 fv3 6206 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 7113 cnvexg 7112 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 7099 dmexg 7097 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 7100 rnexg 7098 |
| [TakeutiZaring] p. 26 | Corollary 6.9(1) | xpexb 38658 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnv 7108 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | fvex 6201 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1-afv 41254 tz6.12-1 6210 tz6.12-afv 41253 tz6.12 6211 tz6.12c 6213 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 6182 tz6.12i 6214 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5891 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5892 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5894 wfo 5886 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5893 wf1 5885 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5895 wf1o 5887 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 6311 eqfnfv2 6312 eqfnfv2f 6315 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 6274 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 6481 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 6479 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5976 funimaexg 5975 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4654 |
| [TakeutiZaring] p. 29 | Definition 6.19(1) | df-so 5036 |
| [TakeutiZaring] p. 30 | Definition 6.21 | dffr2 5079 dffr3 5498 eliniseg 5494 iniseg 5496 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 5029 |
| [TakeutiZaring] p. 30 | Proposition 6.23 | fr2nr 5092 fr3nr 6979 frirr 5091 |
| [TakeutiZaring] p. 30 | Definition 6.24(1) | df-fr 5073 |
| [TakeutiZaring] p. 30 | Definition 6.24(2) | dfwe2 6981 |
| [TakeutiZaring] p. 31 | Exercise 1 | frss 5081 |
| [TakeutiZaring] p. 31 | Exercise 4 | wess 5101 |
| [TakeutiZaring] p. 31 | Proposition 6.26 | tz6.26 5711 tz6.26i 5712 wefrc 5108 wereu2 5111 |
| [TakeutiZaring] p. 32 | Theorem 6.27 | wfi 5713 wfii 5714 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5897 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 6579 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 6580 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 6586 |
| [TakeutiZaring] p. 33 | Proposition 6.31(1) | isomin 6587 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 6588 |
| [TakeutiZaring] p. 33 | Proposition 6.32(1) | isofr 6592 |
| [TakeutiZaring] p. 33 | Proposition 6.32(3) | isowe 6599 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 6601 |
| [TakeutiZaring] p. 35 | Notation | wtr 4752 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | trelpss 38659 tz7.2 5098 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4756 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 5736 |
| [TakeutiZaring] p. 36 | Proposition 7.5 | tz7.5 5744 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 5745 ordelordALT 38747 ordelordALTVD 39103 |
| [TakeutiZaring] p. 37 | Corollary 7.8 | ordelpss 5751 ordelssne 5750 |
| [TakeutiZaring] p. 37 | Proposition 7.7 | tz7.7 5749 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 5753 |
| [TakeutiZaring] p. 38 | Corollary 7.14 | ordeleqon 6988 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 6989 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 5727 |
| [TakeutiZaring] p. 38 | Proposition 7.10 | ordtri3or 5755 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | onfrALT 38764 ordon 6982 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 6984 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 7053 |
| [TakeutiZaring] p. 40 | Exercise 3 | ontr2 5772 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4754 |
| [TakeutiZaring] p. 40 | Exercise 9 | onssmin 6997 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 7031 |
| [TakeutiZaring] p. 40 | Exercise 12 | ordun 5829 |
| [TakeutiZaring] p. 40 | Exercise 14 | ordequn 5828 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 6985 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 4467 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 5729 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 5802 sucidg 5803 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 7013 |
| [TakeutiZaring] p. 41 | Proposition 7.25 | onnbtwn 5818 ordnbtwn 5816 |
| [TakeutiZaring] p. 41 | Proposition 7.26 | onsucuni 7028 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-lim 5728 |
| [TakeutiZaring] p. 42 | Exercise 4 | omssnlim 7079 |
| [TakeutiZaring] p. 42 | Exercise 7 | ssnlim 7083 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 7041 ordelsuc 7020 |
| [TakeutiZaring] p. 42 | Exercise 9 | ordsucelsuc 7022 |
| [TakeutiZaring] p. 42 | Definition 7.27 | nlimon 7051 |
| [TakeutiZaring] p. 42 | Definition 7.28 | dfom2 7067 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 7085 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 7086 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 7087 |
| [TakeutiZaring] p. 43 | Remark | omon 7076 |
| [TakeutiZaring] p. 43 | Axiom 7 | inf3 8532 omex 8540 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 7074 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 7091 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 7088 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 7089 |
| [TakeutiZaring] p. 44 | Exercise 1 | limomss 7070 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 4490 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintss 4769 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 4492 |
| [TakeutiZaring] p. 44 | Exercise 5 | intex 4820 |
| [TakeutiZaring] p. 44 | Exercise 6 | oninton 7000 |
| [TakeutiZaring] p. 44 | Exercise 11 | ordintdif 5774 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 4476 |
| [TakeutiZaring] p. 44 | Proposition 7.34 | noinfep 8557 |
| [TakeutiZaring] p. 45 | Exercise 4 | onint 6995 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 7472 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfr1 7493 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfr2 7494 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfr3 7495 |
| [TakeutiZaring] p. 49 | Theorem 7.44 | tz7.44-1 7502 tz7.44-2 7503 tz7.44-3 7504 |
| [TakeutiZaring] p. 50 | Exercise 1 | smogt 7464 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 7459 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 7443 |
| [TakeutiZaring] p. 51 | Proposition 7.49 | tz7.49 7540 tz7.49c 7541 |
| [TakeutiZaring] p. 51 | Proposition 7.48(1) | tz7.48-1 7538 |
| [TakeutiZaring] p. 51 | Proposition 7.48(2) | tz7.48-2 7537 |
| [TakeutiZaring] p. 51 | Proposition 7.48(3) | tz7.48-3 7539 |
| [TakeutiZaring] p. 53 | Proposition 7.53 | 2eu5 2557 |
| [TakeutiZaring] p. 54 | Proposition 7.56(1) | leweon 8834 |
| [TakeutiZaring] p. 54 | Proposition 7.58(1) | r0weon 8835 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oalim 7612 oasuc 7604 |
| [TakeutiZaring] p. 57 | Remark | tfindsg 7060 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 7615 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 7596 oa0r 7618 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 7616 |
| [TakeutiZaring] p. 58 | Corollary 8.5 | oacan 7628 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 7699 nnaordi 7698 oaord 7627 oaordi 7626 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4565 uniss2 4470 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordri 7630 |
| [TakeutiZaring] p. 59 | Proposition 8.8 | oawordeu 7635 oawordex 7637 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 7691 |
| [TakeutiZaring] p. 59 | Proposition 8.10 | oaabs 7724 |
| [TakeutiZaring] p. 60 | Remark | oancom 8548 |
| [TakeutiZaring] p. 60 | Proposition 8.11 | oalimcl 7640 |
| [TakeutiZaring] p. 62 | Exercise 1 | nnarcl 7696 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 7632 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 7597 om0x 7599 omlim 7613 omsuc 7606 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnecl 7693 nnmcl 7692 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 7712 nnmordi 7711 omord 7648 omordi 7646 |
| [TakeutiZaring] p. 63 | Proposition 8.20 | omcan 7649 |
| [TakeutiZaring] p. 63 | Proposition 8.21 | nnmwordri 7716 omwordri 7652 |
| [TakeutiZaring] p. 63 | Proposition 8.18(1) | om0r 7619 |
| [TakeutiZaring] p. 63 | Proposition 8.18(2) | om1 7622 om1r 7623 |
| [TakeutiZaring] p. 64 | Proposition 8.22 | om00 7655 |
| [TakeutiZaring] p. 64 | Proposition 8.23 | omordlim 7657 |
| [TakeutiZaring] p. 64 | Proposition 8.24 | omlimcl 7658 |
| [TakeutiZaring] p. 64 | Proposition 8.25 | odi 7659 |
| [TakeutiZaring] p. 65 | Theorem 8.26 | omass 7660 |
| [TakeutiZaring] p. 67 | Definition 8.30 | nnesuc 7688 oe0 7602 oelim 7614 oesuc 7607 onesuc 7610 |
| [TakeutiZaring] p. 67 | Proposition 8.31 | oe0m0 7600 |
| [TakeutiZaring] p. 67 | Proposition 8.32 | oen0 7666 |
| [TakeutiZaring] p. 67 | Proposition 8.33 | oeordi 7667 |
| [TakeutiZaring] p. 67 | Proposition 8.31(2) | oe0m1 7601 |
| [TakeutiZaring] p. 67 | Proposition 8.31(3) | oe1m 7625 |
| [TakeutiZaring] p. 68 | Corollary 8.34 | oeord 7668 |
| [TakeutiZaring] p. 68 | Corollary 8.36 | oeordsuc 7674 |
| [TakeutiZaring] p. 68 | Proposition 8.35 | oewordri 7672 |
| [TakeutiZaring] p. 68 | Proposition 8.37 | oeworde 7673 |
| [TakeutiZaring] p. 69 | Proposition 8.41 | oeoa 7677 |
| [TakeutiZaring] p. 70 | Proposition 8.42 | oeoe 7679 |
| [TakeutiZaring] p. 73 | Theorem 9.1 | trcl 8604 tz9.1 8605 |
| [TakeutiZaring] p. 76 | Definition 9.9 | df-r1 8627 r10 8631 r1lim 8635 r1limg 8634 r1suc 8633 r1sucg 8632 |
| [TakeutiZaring] p. 77 | Proposition 9.10(2) | r1ord 8643 r1ord2 8644 r1ordg 8641 |
| [TakeutiZaring] p. 78 | Proposition 9.12 | tz9.12 8653 |
| [TakeutiZaring] p. 78 | Proposition 9.13 | rankwflem 8678 tz9.13 8654 tz9.13g 8655 |
| [TakeutiZaring] p. 79 | Definition 9.14 | df-rank 8628 rankval 8679 rankvalb 8660 rankvalg 8680 |
| [TakeutiZaring] p. 79 | Proposition 9.16 | rankel 8702 rankelb 8687 |
| [TakeutiZaring] p. 79 | Proposition 9.17 | rankuni2b 8716 rankval3 8703 rankval3b 8689 |
| [TakeutiZaring] p. 79 | Proposition 9.18 | rankonid 8692 |
| [TakeutiZaring] p. 79 | Proposition 9.15(1) | rankon 8658 |
| [TakeutiZaring] p. 79 | Proposition 9.15(2) | rankr1 8697 rankr1c 8684 rankr1g 8695 |
| [TakeutiZaring] p. 79 | Proposition 9.15(3) | ssrankr1 8698 |
| [TakeutiZaring] p. 80 | Exercise 1 | rankss 8712 rankssb 8711 |
| [TakeutiZaring] p. 80 | Exercise 2 | unbndrank 8705 |
| [TakeutiZaring] p. 80 | Proposition 9.19 | bndrank 8704 |
| [TakeutiZaring] p. 83 | Axiom of Choice | ac4 9297 dfac3 8944 |
| [TakeutiZaring] p. 84 | Theorem 10.3 | dfac8a 8853 numth 9294 numth2 9293 |
| [TakeutiZaring] p. 85 | Definition 10.4 | cardval 9368 |
| [TakeutiZaring] p. 85 | Proposition 10.5 | cardid 9369 cardid2 8779 |
| [TakeutiZaring] p. 85 | Proposition 10.9 | oncard 8786 |
| [TakeutiZaring] p. 85 | Proposition 10.10 | carden 9373 |
| [TakeutiZaring] p. 85 | Proposition 10.11 | cardidm 8785 |
| [TakeutiZaring] p. 85 | Proposition 10.6(1) | cardon 8770 |
| [TakeutiZaring] p. 85 | Proposition 10.6(2) | cardne 8791 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 8783 |
| [TakeutiZaring] p. 87 | Proposition 10.15 | pwen 8133 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 8019 |
| [TakeutiZaring] p. 88 | Exercise 7 | infensuc 8138 |
| [TakeutiZaring] p. 89 | Exercise 10 | omxpen 8062 |
| [TakeutiZaring] p. 90 | Corollary 10.23 | cardnn 8789 |
| [TakeutiZaring] p. 90 | Definition 10.27 | alephiso 8921 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 8143 |
| [TakeutiZaring] p. 90 | Proposition 10.22 | onomeneq 8150 |
| [TakeutiZaring] p. 90 | Proposition 10.26 | alephprc 8922 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 8148 |
| [TakeutiZaring] p. 91 | Exercise 2 | alephle 8911 |
| [TakeutiZaring] p. 91 | Exercise 3 | aleph0 8889 |
| [TakeutiZaring] p. 91 | Exercise 4 | cardlim 8798 |
| [TakeutiZaring] p. 91 | Exercise 7 | infpss 9039 |
| [TakeutiZaring] p. 91 | Exercise 8 | infcntss 8234 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 7959 isfi 7979 |
| [TakeutiZaring] p. 92 | Proposition 10.32 | onfin 8151 |
| [TakeutiZaring] p. 92 | Proposition 10.34 | imadomg 9356 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 8055 |
| [TakeutiZaring] p. 93 | Proposition 10.35 | fodomb 9348 |
| [TakeutiZaring] p. 93 | Proposition 10.36 | cdaxpdom 9011 unxpdom 8167 |
| [TakeutiZaring] p. 93 | Proposition 10.37 | cardsdomel 8800 cardsdomelir 8799 |
| [TakeutiZaring] p. 93 | Proposition 10.38 | sucxpdom 8169 |
| [TakeutiZaring] p. 94 | Proposition 10.39 | infxpen 8837 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 7859 |
| [TakeutiZaring] p. 95 | Proposition 10.40 | infxpidm 9384 infxpidm2 8840 |
| [TakeutiZaring] p. 95 | Proposition 10.41 | infcda 9030 infxp 9037 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2en 8067 pw2f1o 8065 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 8126 |
| [TakeutiZaring] p. 97 | Theorem 10.46 | ac6s3 9309 |
| [TakeutiZaring] p. 98 | Theorem 10.46 | ac6c5 9304 ac6s5 9313 |
| [TakeutiZaring] p. 98 | Theorem 10.47 | unidom 9365 |
| [TakeutiZaring] p. 99 | Theorem 10.48 | uniimadom 9366 uniimadomf 9367 |
| [TakeutiZaring] p. 100 | Definition 11.1 | cfcof 9096 |
| [TakeutiZaring] p. 101 | Proposition 11.7 | cofsmo 9091 |
| [TakeutiZaring] p. 102 | Exercise 1 | cfle 9076 |
| [TakeutiZaring] p. 102 | Exercise 2 | cf0 9073 |
| [TakeutiZaring] p. 102 | Exercise 3 | cfsuc 9079 |
| [TakeutiZaring] p. 102 | Exercise 4 | cfom 9086 |
| [TakeutiZaring] p. 102 | Proposition 11.9 | coftr 9095 |
| [TakeutiZaring] p. 103 | Theorem 11.15 | alephreg 9404 |
| [TakeutiZaring] p. 103 | Proposition 11.11 | cardcf 9074 |
| [TakeutiZaring] p. 103 | Proposition 11.13 | alephsing 9098 |
| [TakeutiZaring] p. 104 | Corollary 11.17 | cardinfima 8920 |
| [TakeutiZaring] p. 104 | Proposition 11.16 | carduniima 8919 |
| [TakeutiZaring] p. 104 | Proposition 11.18 | alephfp 8931 alephfp2 8932 |
| [TakeutiZaring] p. 106 | Theorem 11.20 | gchina 9521 |
| [TakeutiZaring] p. 106 | Theorem 11.21 | mappwen 8935 |
| [TakeutiZaring] p. 107 | Theorem 11.26 | konigth 9391 |
| [TakeutiZaring] p. 108 | Theorem 11.28 | pwcfsdom 9405 |
| [TakeutiZaring] p. 108 | Theorem 11.29 | cfpwsdom 9406 |
| [Tarski] p. 67 | Axiom B5 | ax-c5 34168 |
| [Tarski] p. 67 | Scheme B5 | sp 2053 |
| [Tarski] p. 68 | Lemma 6 | avril1 27319 equid 1939 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1944 |
| [Tarski] p. 70 | Lemma 14 | spim 2254 spime 2256 spimeh 1925 |
| [Tarski] p. 70 | Lemma 16 | ax-12 2047 ax-c15 34174 ax12i 1879 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 2429 |
| [Tarski] p. 75 | Axiom B7 | ax6v 1889 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-5 1839 ax5ALT 34192 |
| [Tarski], p. 75 | Scheme B8 of system S2 | ax-7 1935 ax-8 1992 ax-9 1999 |
| [Tarski1999] p. 178 | Axiom 4 | axtgsegcon 25363 |
| [Tarski1999] p. 178 | Axiom 5 | axtg5seg 25364 |
| [Tarski1999] p. 179 | Axiom 7 | axtgpasch 25366 |
| [Tarski1999] p. 180 | Axiom 7.1 | axtgpasch 25366 |
| [Tarski1999] p. 185 | Axiom 11 | axtgcont1 25367 |
| [Truss] p. 114 | Theorem 5.18 | ruc 14972 |
| [Viaclovsky7] p. 3 | Corollary 0.3 | mblfinlem3 33448 |
| [Viaclovsky8] p. 3 | Proposition 7 | ismblfin 33450 |
| [Weierstrass] p. 272 | Definition | df-mdet 20391 mdetuni 20428 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 | pm1.2 535 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 399 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 401 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 544 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 886 |
| [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 130 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 90 wl-pm2.04 33267 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | frege5 38094 imim2 58 wl-imim2 33262 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 83 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1 433 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2563 syl 17 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 411 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 22 wl-id 33265 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmid 431 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 136 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13 434 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotr 125 notnotrALT2 39163 wl-notnotr 33266 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1 143 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | ax-frege28 38124 axfrege28 38123 con3 149 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | ax-3 8 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18 122 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 400 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 596 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 120 wl-pm2.21 33259 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 121 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25 419 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26 927 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | conventions-label 27259 pm2.27 42 wl-pm2.27 33257 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 547 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 548 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 888 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 889 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 887 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1038 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 599 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 597 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 598 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 56 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 412 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 413 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5 164 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6 182 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 414 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 415 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 416 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 165 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 167 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 388 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54 389 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 397 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 398 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61 183 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 425 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 829 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 830 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 184 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 417 pm2.67 418 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521 166 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 424 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 895 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68 426 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinv 194 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 890 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 891 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 894 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 893 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 896 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 897 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 84 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85 898 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 108 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 519 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 463 pm3.2im 157 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11 520 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12 521 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13 522 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 523 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 464 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 465 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 926 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 611 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 460 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 461 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 473 simplim 163 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 477 simprim 162 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 609 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 610 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 603 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 879 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 584 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 582 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 583 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 534 pm3.44 533 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | prth 595 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 906 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 878 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34b 306 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 251 |
| [WhiteheadRussell] p. 117 | Theorem *4.11 | notbi 309 |
| [WhiteheadRussell] p. 117 | Theorem *4.12 | con2bi 343 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotb 304 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14 602 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 605 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 212 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 972 bitr 745 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 675 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 536 pm4.25 537 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 911 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 402 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 681 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 546 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 743 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 742 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 916 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 915 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1039 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 908 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42 1004 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 968 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 601 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 900 pm4.45 724 pm4.45im 585 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anor 510 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imor 428 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 570 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianor 509 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52 512 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53 513 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54 514 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55 515 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 511 pm4.56 516 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | oran 517 pm4.57 518 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | pm4.61 442 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62 435 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63 437 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64 387 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65 443 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66 436 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67 444 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 662 pm4.71d 666 pm4.71i 664 pm4.71r 663 pm4.71rd 667 pm4.71ri 665 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 920 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 524 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 420 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 907 pm4.76 910 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 822 pm4.77 828 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78 606 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79 607 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 380 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81 381 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 969 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83 970 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 337 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 338 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 341 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 376 impexp 462 pm4.87 608 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 902 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11 928 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12 929 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13 931 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14 930 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15 933 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 934 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17 932 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbn 373 pm5.18 371 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 375 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 903 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xor 935 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3 994 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24 996 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2 427 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 748 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 377 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 351 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6 951 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7 975 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 612 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 668 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 922 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 942 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 923 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 378 pm5.41 379 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 571 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 950 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 837 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54 943 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55 939 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 749 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62 958 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63 959 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71 977 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 356 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 259 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 978 |
| [WhiteheadRussell] p. 146 | Theorem *10.12 | pm10.12 38557 |
| [WhiteheadRussell] p. 146 | Theorem *10.14 | pm10.14 38558 |
| [WhiteheadRussell] p. 147 | Theorem *10.22 | 19.26 1798 |
| [WhiteheadRussell] p. 149 | Theorem *10.251 | pm10.251 38559 |
| [WhiteheadRussell] p. 149 | Theorem *10.252 | pm10.252 38560 |
| [WhiteheadRussell] p. 149 | Theorem *10.253 | pm10.253 38561 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1820 |
| [WhiteheadRussell] p. 151 | Theorem *10.301 | albitr 38562 |
| [WhiteheadRussell] p. 155 | Theorem *10.42 | pm10.42 38563 |
| [WhiteheadRussell] p. 155 | Theorem *10.52 | pm10.52 38564 |
| [WhiteheadRussell] p. 155 | Theorem *10.53 | pm10.53 38565 |
| [WhiteheadRussell] p. 155 | Theorem *10.541 | pm10.541 38566 |
| [WhiteheadRussell] p. 156 | Theorem *10.55 | pm10.55 38568 |
| [WhiteheadRussell] p. 156 | Theorem *10.56 | pm10.56 38569 |
| [WhiteheadRussell] p. 156 | Theorem *10.57 | pm10.57 38570 |
| [WhiteheadRussell] p. 156 | Theorem *10.542 | pm10.542 38567 |
| [WhiteheadRussell] p. 159 | Axiom *11.07 | pm11.07 2447 |
| [WhiteheadRussell] p. 159 | Theorem *11.11 | pm11.11 38573 |
| [WhiteheadRussell] p. 159 | Theorem *11.12 | pm11.12 38574 |
| [WhiteheadRussell] p. 159 | Theorem PM*11.1 | 2stdpc4 2354 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 2038 |
| [WhiteheadRussell] p. 160 | Theorem *11.22 | 2exnaln 1756 |
| [WhiteheadRussell] p. 160 | Theorem *11.25 | 2nexaln 1757 |
| [WhiteheadRussell] p. 161 | Theorem *11.3 | 19.21vv 38575 |
| [WhiteheadRussell] p. 162 | Theorem *11.32 | 2alim 38576 |
| [WhiteheadRussell] p. 162 | Theorem *11.33 | 2albi 38577 |
| [WhiteheadRussell] p. 162 | Theorem *11.34 | 2exim 38578 |
| [WhiteheadRussell] p. 162 | Theorem *11.36 | spsbce-2 38580 |
| [WhiteheadRussell] p. 162 | Theorem *11.341 | 2exbi 38579 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1814 |
| [WhiteheadRussell] p. 163 | Theorem *11.43 | 19.36vv 38582 |
| [WhiteheadRussell] p. 163 | Theorem *11.44 | 19.31vv 38583 |
| [WhiteheadRussell] p. 163 | Theorem *11.421 | 19.33-2 38581 |
| [WhiteheadRussell] p. 164 | Theorem *11.5 | 2nalexn 1755 |
| [WhiteheadRussell] p. 164 | Theorem *11.46 | 19.37vv 38584 |
| [WhiteheadRussell] p. 164 | Theorem *11.47 | 19.28vv 38585 |
| [WhiteheadRussell] p. 164 | Theorem *11.51 | 2exnexn 1772 |
| [WhiteheadRussell] p. 164 | Theorem *11.52 | pm11.52 38586 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 2179 |
| [WhiteheadRussell] p. 164 | Theorem *11.521 | 2exanali 38587 |
| [WhiteheadRussell] p. 165 | Theorem *11.6 | pm11.6 38592 |
| [WhiteheadRussell] p. 165 | Theorem *11.56 | aaanv 38588 |
| [WhiteheadRussell] p. 165 | Theorem *11.57 | pm11.57 38589 |
| [WhiteheadRussell] p. 165 | Theorem *11.58 | pm11.58 38590 |
| [WhiteheadRussell] p. 165 | Theorem *11.59 | pm11.59 38591 |
| [WhiteheadRussell] p. 166 | Theorem *11.7 | pm11.7 38596 |
| [WhiteheadRussell] p. 166 | Theorem *11.61 | pm11.61 38593 |
| [WhiteheadRussell] p. 166 | Theorem *11.62 | pm11.62 38594 |
| [WhiteheadRussell] p. 166 | Theorem *11.63 | pm11.63 38595 |
| [WhiteheadRussell] p. 166 | Theorem *11.71 | pm11.71 38597 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2474 |
| [WhiteheadRussell] p. 178 | Theorem *13.13 | pm13.13a 38608 pm13.13b 38609 |
| [WhiteheadRussell] p. 178 | Theorem *13.14 | pm13.14 38610 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2875 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2876 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 3344 |
| [WhiteheadRussell] p. 179 | Theorem *13.21 | 2sbc6g 38616 |
| [WhiteheadRussell] p. 179 | Theorem *13.22 | 2sbc5g 38617 |
| [WhiteheadRussell] p. 179 | Theorem *13.192 | pm13.192 38611 |
| [WhiteheadRussell] p. 179 | Theorem *13.193 | 2pm13.193 38768 pm13.193 38612 |
| [WhiteheadRussell] p. 179 | Theorem *13.194 | pm13.194 38613 |
| [WhiteheadRussell] p. 179 | Theorem *13.195 | pm13.195 38614 |
| [WhiteheadRussell] p. 179 | Theorem *13.196 | pm13.196a 38615 |
| [WhiteheadRussell] p. 184 | Theorem *14.12 | pm14.12 38622 |
| [WhiteheadRussell] p. 184 | Theorem *14.111 | iotasbc2 38621 |
| [WhiteheadRussell] p. 184 | Definition *14.01 | iotasbc 38620 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3488 |
| [WhiteheadRussell] p. 185 | Theorem *14.122 | pm14.122a 38623 pm14.122b 38624 pm14.122c 38625 |
| [WhiteheadRussell] p. 185 | Theorem *14.123 | pm14.123a 38626 pm14.123b 38627 pm14.123c 38628 |
| [WhiteheadRussell] p. 189 | Theorem *14.2 | iotaequ 38630 |
| [WhiteheadRussell] p. 189 | Theorem *14.18 | pm14.18 38629 |
| [WhiteheadRussell] p. 189 | Theorem *14.202 | iotavalb 38631 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5869 |
| [WhiteheadRussell] p. 190 | Theorem *14.205 | iotasbc5 38632 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5870 |
| [WhiteheadRussell] p. 191 | Theorem *14.24 | pm14.24 38633 |
| [WhiteheadRussell] p. 192 | Theorem *14.25 | sbiota1 38635 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2536 eupickbi 2539 sbaniota 38636 |
| [WhiteheadRussell] p. 192 | Theorem *14.242 | iotavalsb 38634 |
| [WhiteheadRussell] p. 192 | Theorem *14.271 | eubi 38637 |
| [WhiteheadRussell] p. 193 | Theorem *14.272 | iotasbcq 38638 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | conventions 27258 df-fv 5896 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 8826 pm54.43lem 8825 |
| [Young] p. 141 | Definition of operator ordering | leop2 28983 |
| [Young] p. 142 | Example 12.2(i) | 0leop 28989 idleop 28990 |
| [vandenDries] p. 42 | Lemma 61 | irrapx1 37392 |
| [vandenDries] p. 43 | Theorem 62 | pellex 37399 pellexlem1 37393 |