Bibliographic Cross-Reference for the Metamath Proof Explorer
Bibliographic Reference | Description | Metamath Proof Explorer Page(s) |
[Adamek] p.
21 | Definition 3.1 | df-cat 16152 |
[Adamek] p. 21 | Condition
3.1(b) | df-cat 16152 |
[Adamek] p. 22 | Example
3.3(1) | df-setc 16549 |
[Adamek] p. 24 | Example
3.3(4.c) | 0cat 16172 |
[Adamek] p.
25 | Definition 3.5 | df-oppc 16195 |
[Adamek] p. 28 | Remark
3.9 | oppciso 16264 |
[Adamek] p. 28 | Remark
3.12 | invf1o 16252 invisoinvl 16273 |
[Adamek] p. 28 | Example
3.13 | idinv 16272 idiso 16271 |
[Adamek] p. 28 | Corollary
3.11 | inveq 16257 |
[Adamek] p.
28 | Definition 3.8 | df-inv 16231 df-iso 16232 dfiso2 16255 |
[Adamek] p.
28 | Proposition 3.10 | sectcan 16238 |
[Adamek] p. 29 | Remark
3.16 | cicer 16289 |
[Adamek] p.
29 | Definition 3.15 | cic 16282 df-cic 16279 |
[Adamek] p.
29 | Definition 3.17 | df-func 16341 |
[Adamek] p.
29 | Proposition 3.14(1) | invinv 16253 |
[Adamek] p.
29 | Proposition 3.14(2) | invco 16254 isoco 16260 |
[Adamek] p. 30 | Remark
3.19 | df-func 16341 |
[Adamek] p. 30 | Example
3.20(1) | idfucl 16364 |
[Adamek] p.
32 | Proposition 3.21 | funciso 16357 |
[Adamek] p.
33 | Proposition 3.23 | cofucl 16371 |
[Adamek] p. 34 | Remark
3.28(2) | catciso 16580 |
[Adamek] p. 34 | Remark
3.28 (1) | embedsetcestrc 16630 |
[Adamek] p.
34 | Definition 3.27(2) | df-fth 16388 |
[Adamek] p.
34 | Definition 3.27(3) | df-full 16387 |
[Adamek] p.
34 | Definition 3.27 (1) | embedsetcestrc 16630 |
[Adamek] p. 35 | Corollary
3.32 | ffthiso 16412 |
[Adamek] p.
35 | Proposition 3.30(c) | cofth 16418 |
[Adamek] p.
35 | Proposition 3.30(d) | cofull 16417 |
[Adamek] p.
36 | Definition 3.33 (1) | equivestrcsetc 16615 |
[Adamek] p.
36 | Definition 3.33 (2) | equivestrcsetc 16615 |
[Adamek] p.
39 | Definition 3.41 | funcoppc 16358 |
[Adamek] p.
39 | Definition 3.44. | df-catc 16568 |
[Adamek] p.
39 | Proposition 3.43(c) | fthoppc 16406 |
[Adamek] p.
39 | Proposition 3.43(d) | fulloppc 16405 |
[Adamek] p. 40 | Remark
3.48 | catccat 16577 |
[Adamek] p.
40 | Definition 3.47 | df-catc 16568 |
[Adamek] p. 48 | Example
4.3(1.a) | 0subcat 16321 |
[Adamek] p. 48 | Example
4.3(1.b) | catsubcat 16322 |
[Adamek] p.
48 | Definition 4.1(2) | fullsubc 16333 |
[Adamek] p.
48 | Definition 4.1(a) | df-subc 16295 |
[Adamek] p. 49 | Remark
4.4(2) | ressffth 16421 |
[Adamek] p.
83 | Definition 6.1 | df-nat 16426 |
[Adamek] p. 87 | Remark
6.14(a) | fuccocl 16447 |
[Adamek] p. 87 | Remark
6.14(b) | fucass 16451 |
[Adamek] p.
87 | Definition 6.15 | df-fuc 16427 |
[Adamek] p. 88 | Remark
6.16 | fuccat 16453 |
[Adamek] p.
101 | Definition 7.1 | df-inito 16464 |
[Adamek] p.
101 | Example 7.2 (6) | irinitoringc 41861 |
[Adamek] p.
102 | Definition 7.4 | df-termo 16465 |
[Adamek] p.
102 | Proposition 7.3 (1) | initoeu1w 16485 |
[Adamek] p.
102 | Proposition 7.3 (2) | initoeu2 16489 |
[Adamek] p.
103 | Definition 7.7 | df-zeroo 16466 |
[Adamek] p.
103 | Example 7.9 (3) | nzerooringczr 41864 |
[Adamek] p.
103 | Proposition 7.6 | termoeu1w 16492 |
[Adamek] p.
106 | Definition 7.19 | df-sect 16230 |
[Adamek] p.
478 | Item Rng | df-ringc 41797 |
[AhoHopUll]
p. 2 | Section 1.1 | df-bigo 42140 |
[AhoHopUll]
p. 12 | Section 1.3 | df-blen 42162 |
[AhoHopUll] p.
318 | Section 9.1 | df-concat 13156 df-pfx 40245 df-substr 13158 df-word 13154 lencl 13179 wrd0 13185 |
[AkhiezerGlazman] p.
39 | Linear operator norm | df-nmo 22322 df-nmoo 26984 |
[AkhiezerGlazman] p.
64 | Theorem | hmopidmch 28396 hmopidmchi 28394 |
[AkhiezerGlazman] p. 65 | Theorem
1 | pjcmul1i 28444 pjcmul2i 28445 |
[AkhiezerGlazman] p.
72 | Theorem | cnvunop 28161 unoplin 28163 |
[AkhiezerGlazman] p. 72 | Equation
2 | unopadj 28162 unopadj2 28181 |
[AkhiezerGlazman] p.
73 | Theorem | elunop2 28256 lnopunii 28255 |
[AkhiezerGlazman] p.
80 | Proposition 1 | adjlnop 28329 |
[Apostol] p. 18 | Theorem
I.1 | addcan 10099 addcan2d 10119 addcan2i 10109 addcand 10118 addcani 10108 |
[Apostol] p. 18 | Theorem
I.2 | negeu 10150 |
[Apostol] p. 18 | Theorem
I.3 | negsub 10208 negsubd 10277 negsubi 10238 |
[Apostol] p. 18 | Theorem
I.4 | negneg 10210 negnegd 10262 negnegi 10230 |
[Apostol] p. 18 | Theorem
I.5 | subdi 10342 subdid 10365 subdii 10358 subdir 10343 subdird 10366 subdiri 10359 |
[Apostol] p. 18 | Theorem
I.6 | mul01 10094 mul01d 10114 mul01i 10105 mul02 10093 mul02d 10113 mul02i 10104 |
[Apostol] p. 18 | Theorem
I.7 | mulcan 10543 mulcan2d 10540 mulcand 10539 mulcani 10545 |
[Apostol] p. 18 | Theorem
I.8 | receu 10551 xreceu 28961 |
[Apostol] p. 18 | Theorem
I.9 | divrec 10580 divrecd 10683 divreci 10649 divreczi 10642 |
[Apostol] p. 18 | Theorem
I.10 | recrec 10601 recreci 10636 |
[Apostol] p. 18 | Theorem
I.11 | mul0or 10546 mul0ord 10556 mul0ori 10554 |
[Apostol] p. 18 | Theorem
I.12 | mul2neg 10348 mul2negd 10364 mul2negi 10357 mulneg1 10345 mulneg1d 10362 mulneg1i 10355 |
[Apostol] p. 18 | Theorem
I.13 | divadddiv 10619 divadddivd 10724 divadddivi 10666 |
[Apostol] p. 18 | Theorem
I.14 | divmuldiv 10604 divmuldivd 10721 divmuldivi 10664 rdivmuldivd 29122 |
[Apostol] p. 18 | Theorem
I.15 | divdivdiv 10605 divdivdivd 10727 divdivdivi 10667 |
[Apostol] p. 20 | Axiom
7 | rpaddcl 11730 rpaddcld 11763 rpmulcl 11731 rpmulcld 11764 |
[Apostol] p. 20 | Axiom
8 | rpneg 11739 |
[Apostol] p. 20 | Axiom
9 | 0nrp 11741 |
[Apostol] p. 20 | Theorem
I.17 | lttri 10042 |
[Apostol] p. 20 | Theorem
I.18 | ltadd1d 10499 ltadd1dd 10517 ltadd1i 10461 |
[Apostol] p. 20 | Theorem
I.19 | ltmul1 10752 ltmul1a 10751 ltmul1i 10821 ltmul1ii 10831 ltmul2 10753 ltmul2d 11790 ltmul2dd 11804 ltmul2i 10824 |
[Apostol] p. 20 | Theorem
I.20 | msqgt0 10427 msqgt0d 10474 msqgt0i 10444 |
[Apostol] p. 20 | Theorem
I.21 | 0lt1 10429 |
[Apostol] p. 20 | Theorem
I.23 | lt0neg1 10413 lt0neg1d 10476 ltneg 10407 ltnegd 10484 ltnegi 10451 |
[Apostol] p. 20 | Theorem
I.25 | lt2add 10392 lt2addd 10529 lt2addi 10469 |
[Apostol] p.
20 | Definition of positive numbers | df-rp 11709 |
[Apostol] p.
21 | Exercise 4 | recgt0 10746 recgt0d 10837 recgt0i 10807 recgt0ii 10808 |
[Apostol] p.
22 | Definition of integers | df-z 11255 |
[Apostol] p.
22 | Definition of positive integers | dfnn3 10911 |
[Apostol] p.
22 | Definition of rationals | df-q 11665 |
[Apostol] p. 24 | Theorem
I.26 | supeu 8243 |
[Apostol] p. 26 | Theorem
I.28 | nnunb 11165 |
[Apostol] p. 26 | Theorem
I.29 | arch 11166 |
[Apostol] p.
28 | Exercise 2 | btwnz 11355 |
[Apostol] p.
28 | Exercise 3 | nnrecl 11167 |
[Apostol] p.
28 | Exercise 4 | rebtwnz 11663 |
[Apostol] p.
28 | Exercise 5 | zbtwnre 11662 |
[Apostol] p.
28 | Exercise 6 | qbtwnre 11904 |
[Apostol] p.
28 | Exercise 10(a) | zeneo 14901 zneo 11336 zneoALTV 40118 |
[Apostol] p. 29 | Theorem
I.35 | msqsqrtd 14027 resqrtth 13844 sqrtth 13952 sqrtthi 13958 sqsqrtd 14026 |
[Apostol] p. 34 | Theorem
I.36 (principle of mathematical induction) | peano5nni 10900 |
[Apostol] p. 34 | Theorem
I.37 (well-ordering principle) | nnwo 11629 |
[Apostol] p.
361 | Remark | crreczi 12851 |
[Apostol] p.
363 | Remark | absgt0i 13986 |
[Apostol] p.
363 | Example | abssubd 14040 abssubi 13990 |
[ApostolNT]
p. 7 | Remark | fmtno0 39990 fmtno1 39991 fmtno2 40000 fmtno3 40001 fmtno4 40002 fmtno5fac 40032 fmtnofz04prm 40027 |
[ApostolNT]
p. 7 | Definition | df-fmtno 39978 |
[ApostolNT] p.
8 | Definition | df-ppi 24626 |
[ApostolNT] p.
14 | Definition | df-dvds 14822 |
[ApostolNT] p.
14 | Theorem 1.1(a) | iddvds 14833 |
[ApostolNT] p.
14 | Theorem 1.1(b) | dvdstr 14856 |
[ApostolNT] p.
14 | Theorem 1.1(c) | dvds2ln 14852 |
[ApostolNT] p.
14 | Theorem 1.1(d) | dvdscmul 14846 |
[ApostolNT] p.
14 | Theorem 1.1(e) | dvdscmulr 14848 |
[ApostolNT] p.
14 | Theorem 1.1(f) | 1dvds 14834 |
[ApostolNT] p.
14 | Theorem 1.1(g) | dvds0 14835 |
[ApostolNT] p.
14 | Theorem 1.1(h) | 0dvds 14840 |
[ApostolNT] p.
14 | Theorem 1.1(i) | dvdsleabs 14871 |
[ApostolNT] p.
14 | Theorem 1.1(j) | dvdsabseq 14873 |
[ApostolNT] p.
14 | Theorem 1.1(k) | divconjdvds 14875 |
[ApostolNT] p.
15 | Definition | df-gcd 15055 dfgcd2 15101 |
[ApostolNT] p.
16 | Definition | isprm2 15233 |
[ApostolNT] p.
16 | Theorem 1.5 | coprmdvds 15204 |
[ApostolNT] p.
16 | Theorem 1.7 | prminf 15457 |
[ApostolNT] p.
16 | Theorem 1.4(a) | gcdcom 15073 |
[ApostolNT] p.
16 | Theorem 1.4(b) | gcdass 15102 |
[ApostolNT] p.
16 | Theorem 1.4(c) | absmulgcd 15104 |
[ApostolNT] p.
16 | Theorem 1.4(d)1 | gcd1 15087 |
[ApostolNT] p.
16 | Theorem 1.4(d)2 | gcdid0 15079 |
[ApostolNT] p.
17 | Theorem 1.8 | coprm 15261 |
[ApostolNT] p.
17 | Theorem 1.9 | euclemma 15263 |
[ApostolNT] p.
17 | Theorem 1.10 | 1arith2 15470 |
[ApostolNT] p.
18 | Theorem 1.13 | prmrec 15464 |
[ApostolNT] p.
19 | Theorem 1.14 | divalg 14964 |
[ApostolNT] p.
20 | Theorem 1.15 | eucalg 15138 |
[ApostolNT] p.
24 | Definition | df-mu 24627 |
[ApostolNT] p.
25 | Definition | df-phi 15309 |
[ApostolNT] p.
25 | Theorem 2.1 | musum 24717 |
[ApostolNT] p.
26 | Theorem 2.2 | phisum 15333 |
[ApostolNT] p.
28 | Theorem 2.5(a) | phiprmpw 15319 |
[ApostolNT] p.
28 | Theorem 2.5(c) | phimul 15323 |
[ApostolNT] p.
32 | Definition | df-vma 24624 |
[ApostolNT] p.
32 | Theorem 2.9 | muinv 24719 |
[ApostolNT] p.
32 | Theorem 2.10 | vmasum 24741 |
[ApostolNT] p.
38 | Remark | df-sgm 24628 |
[ApostolNT] p.
38 | Definition | df-sgm 24628 |
[ApostolNT] p.
75 | Definition | df-chp 24625 df-cht 24623 |
[ApostolNT] p.
104 | Definition | congr 15216 |
[ApostolNT] p.
106 | Remark | dvdsval3 14825 |
[ApostolNT] p.
106 | Definition | moddvds 14829 |
[ApostolNT] p.
107 | Example 2 | mod2eq0even 14908 |
[ApostolNT] p.
107 | Example 3 | mod2eq1n2dvds 14909 |
[ApostolNT] p.
107 | Example 4 | zmod1congr 12549 |
[ApostolNT] p.
107 | Theorem 5.2(b) | modmul12d 12586 |
[ApostolNT] p.
107 | Theorem 5.2(c) | modexp 12861 |
[ApostolNT] p.
108 | Theorem 5.3 | modmulconst 14851 |
[ApostolNT] p.
109 | Theorem 5.4 | cncongr1 15219 |
[ApostolNT] p.
109 | Theorem 5.6 | gcdmodi 15616 |
[ApostolNT] p.
109 | Theorem 5.4 "Cancellation law" | cncongr 15221 |
[ApostolNT] p.
113 | Theorem 5.17 | eulerth 15326 |
[ApostolNT] p.
113 | Theorem 5.18 | vfermltl 15344 |
[ApostolNT] p.
114 | Theorem 5.19 | fermltl 15327 |
[ApostolNT] p.
116 | Theorem 5.24 | wilthimp 24598 |
[ApostolNT] p.
179 | Definition | df-lgs 24820 lgsprme0 24864 |
[ApostolNT] p.
180 | Example 1 | 1lgs 24865 |
[ApostolNT] p.
180 | Theorem 9.2 | lgsvalmod 24841 |
[ApostolNT] p.
180 | Theorem 9.3 | lgsdirprm 24856 |
[ApostolNT] p.
181 | Theorem 9.4 | m1lgs 24913 |
[ApostolNT] p.
181 | Theorem 9.5 | 2lgs 24932 2lgsoddprm 24941 |
[ApostolNT] p.
182 | Theorem 9.6 | gausslemma2d 24899 |
[ApostolNT] p.
185 | Theorem 9.8 | lgsquad 24908 |
[ApostolNT] p.
188 | Definition | df-lgs 24820 lgs1 24866 |
[ApostolNT] p.
188 | Theorem 9.9(a) | lgsdir 24857 |
[ApostolNT] p.
188 | Theorem 9.9(b) | lgsdi 24859 |
[ApostolNT] p.
188 | Theorem 9.9(c) | lgsmodeq 24867 |
[ApostolNT] p.
188 | Theorem 9.9(d) | lgsmulsqcoprm 24868 |
[Baer] p.
40 | Property (b) | mapdord 35945 |
[Baer] p.
40 | Property (c) | mapd11 35946 |
[Baer] p.
40 | Property (e) | mapdin 35969 mapdlsm 35971 |
[Baer] p.
40 | Property (f) | mapd0 35972 |
[Baer] p.
40 | Definition of projectivity | df-mapd 35932 mapd1o 35955 |
[Baer] p.
41 | Property (g) | mapdat 35974 |
[Baer] p.
44 | Part (1) | mapdpg 36013 |
[Baer] p.
45 | Part (2) | hdmap1eq 36109 mapdheq 36035 mapdheq2 36036 mapdheq2biN 36037 |
[Baer] p.
45 | Part (3) | baerlem3 36020 |
[Baer] p.
46 | Part (4) | mapdheq4 36039 mapdheq4lem 36038 |
[Baer] p.
46 | Part (5) | baerlem5a 36021 baerlem5abmN 36025 baerlem5amN 36023 baerlem5b 36022 baerlem5bmN 36024 |
[Baer] p.
47 | Part (6) | hdmap1l6 36129 hdmap1l6a 36117 hdmap1l6e 36122 hdmap1l6f 36123 hdmap1l6g 36124 hdmap1l6lem1 36115 hdmap1l6lem2 36116 hdmap1p6N 36130 mapdh6N 36054 mapdh6aN 36042 mapdh6eN 36047 mapdh6fN 36048 mapdh6gN 36049 mapdh6lem1N 36040 mapdh6lem2N 36041 |
[Baer] p.
48 | Part 9 | hdmapval 36138 |
[Baer] p.
48 | Part 10 | hdmap10 36150 |
[Baer] p.
48 | Part 11 | hdmapadd 36153 |
[Baer] p.
48 | Part (6) | hdmap1l6h 36125 mapdh6hN 36050 |
[Baer] p.
48 | Part (7) | mapdh75cN 36060 mapdh75d 36061 mapdh75e 36059 mapdh75fN 36062 mapdh7cN 36056 mapdh7dN 36057 mapdh7eN 36055 mapdh7fN 36058 |
[Baer] p.
48 | Part (8) | mapdh8 36096 mapdh8a 36082 mapdh8aa 36083 mapdh8ab 36084 mapdh8ac 36085 mapdh8ad 36086 mapdh8b 36087 mapdh8c 36088 mapdh8d 36090 mapdh8d0N 36089 mapdh8e 36091 mapdh8fN 36092 mapdh8g 36093 mapdh8i 36094 mapdh8j 36095 |
[Baer] p.
48 | Part (9) | mapdh9a 36097 |
[Baer] p.
48 | Equation 10 | mapdhvmap 36076 |
[Baer] p.
49 | Part 12 | hdmap11 36158 hdmapeq0 36154 hdmapf1oN 36175 hdmapneg 36156 hdmaprnN 36174 hdmaprnlem1N 36159 hdmaprnlem3N 36160 hdmaprnlem3uN 36161 hdmaprnlem4N 36163 hdmaprnlem6N 36164 hdmaprnlem7N 36165 hdmaprnlem8N 36166 hdmaprnlem9N 36167 hdmapsub 36157 |
[Baer] p.
49 | Part 14 | hdmap14lem1 36178 hdmap14lem10 36187 hdmap14lem1a 36176 hdmap14lem2N 36179 hdmap14lem2a 36177 hdmap14lem3 36180 hdmap14lem8 36185 hdmap14lem9 36186 |
[Baer] p.
50 | Part 14 | hdmap14lem11 36188 hdmap14lem12 36189 hdmap14lem13 36190 hdmap14lem14 36191 hdmap14lem15 36192 hgmapval 36197 |
[Baer] p.
50 | Part 15 | hgmapadd 36204 hgmapmul 36205 hgmaprnlem2N 36207 hgmapvs 36201 |
[Baer] p.
50 | Part 16 | hgmaprnN 36211 |
[Baer] p.
110 | Lemma 1 | hdmapip0com 36227 |
[Baer] p.
110 | Line 27 | hdmapinvlem1 36228 |
[Baer] p.
110 | Line 28 | hdmapinvlem2 36229 |
[Baer] p.
110 | Line 30 | hdmapinvlem3 36230 |
[Baer] p.
110 | Part 1.2 | hdmapglem5 36232 hgmapvv 36236 |
[Baer] p.
110 | Proposition 1 | hdmapinvlem4 36231 |
[Baer] p.
111 | Line 10 | hgmapvvlem1 36233 |
[Baer] p.
111 | Line 15 | hdmapg 36240 hdmapglem7 36239 |
[BellMachover] p.
36 | Lemma 10.3 | idALT 23 |
[BellMachover] p.
97 | Definition 10.1 | df-eu 2462 |
[BellMachover] p.
460 | Notation | df-mo 2463 |
[BellMachover] p.
460 | Definition | mo3 2495 |
[BellMachover] p.
461 | Axiom Ext | ax-ext 2590 |
[BellMachover] p.
462 | Theorem 1.1 | bm1.1 2595 |
[BellMachover] p.
463 | Axiom Rep | axrep5 4704 |
[BellMachover] p.
463 | Scheme Sep | axsep 4708 |
[BellMachover] p.
463 | Theorem 1.3ii | bm1.3ii 4712 |
[BellMachover] p.
466 | Problem | axpow2 4771 |
[BellMachover] p.
466 | Axiom Pow | axpow3 4772 |
[BellMachover] p.
466 | Axiom Union | axun2 6849 |
[BellMachover] p.
468 | Definition | df-ord 5643 |
[BellMachover] p.
469 | Theorem 2.2(i) | ordirr 5658 |
[BellMachover] p.
469 | Theorem 2.2(iii) | onelon 5665 |
[BellMachover] p.
469 | Theorem 2.2(vii) | ordn2lp 5660 |
[BellMachover] p.
471 | Definition of N | df-om 6958 |
[BellMachover] p.
471 | Problem 2.5(ii) | bm2.5ii 6898 |
[BellMachover] p.
471 | Definition of Lim | df-lim 5645 |
[BellMachover] p.
472 | Axiom Inf | zfinf2 8422 |
[BellMachover] p.
473 | Theorem 2.8 | limom 6972 |
[BellMachover] p.
477 | Equation 3.1 | df-r1 8510 |
[BellMachover] p.
478 | Definition | rankval2 8564 |
[BellMachover] p.
478 | Theorem 3.3(i) | r1ord3 8528 r1ord3g 8525 |
[BellMachover] p.
480 | Axiom Reg | zfreg 8383 |
[BellMachover] p.
488 | Axiom AC | ac5 9182 dfac4 8828 |
[BellMachover] p.
490 | Definition of aleph | alephval3 8816 |
[BeltramettiCassinelli] p.
98 | Remark | atlatmstc 33624 |
[BeltramettiCassinelli] p.
107 | Remark 10.3.5 | atom1d 28596 |
[BeltramettiCassinelli] p.
166 | Theorem 14.8.4 | chirred 28638 chirredi 28637 |
[BeltramettiCassinelli1] p.
400 | Proposition P8(ii) | atoml2i 28626 |
[Beran] p.
3 | Definition of join | sshjval3 27597 |
[Beran] p.
39 | Theorem 2.3(i) | cmcm2 27859 cmcm2i 27836 cmcm2ii 27841 cmt2N 33555 |
[Beran] p.
40 | Theorem 2.3(iii) | lecm 27860 lecmi 27845 lecmii 27846 |
[Beran] p.
45 | Theorem 3.4 | cmcmlem 27834 |
[Beran] p.
49 | Theorem 4.2 | cm2j 27863 cm2ji 27868 cm2mi 27869 |
[Beran] p.
95 | Definition | df-sh 27448 issh2 27450 |
[Beran] p.
95 | Lemma 3.1(S5) | his5 27327 |
[Beran] p.
95 | Lemma 3.1(S6) | his6 27340 |
[Beran] p.
95 | Lemma 3.1(S7) | his7 27331 |
[Beran] p.
95 | Lemma 3.2(S8) | ho01i 28071 |
[Beran] p.
95 | Lemma 3.2(S9) | hoeq1 28073 |
[Beran] p.
95 | Lemma 3.2(S10) | ho02i 28072 |
[Beran] p.
95 | Lemma 3.2(S11) | hoeq2 28074 |
[Beran] p.
95 | Postulate (S1) | ax-his1 27323 his1i 27341 |
[Beran] p.
95 | Postulate (S2) | ax-his2 27324 |
[Beran] p.
95 | Postulate (S3) | ax-his3 27325 |
[Beran] p.
95 | Postulate (S4) | ax-his4 27326 |
[Beran] p.
96 | Definition of norm | df-hnorm 27209 dfhnorm2 27363 normval 27365 |
[Beran] p.
96 | Definition for Cauchy sequence | hcau 27425 |
[Beran] p.
96 | Definition of Cauchy sequence | df-hcau 27214 |
[Beran] p.
96 | Definition of complete subspace | isch3 27482 |
[Beran] p.
96 | Definition of converge | df-hlim 27213 hlimi 27429 |
[Beran] p.
97 | Theorem 3.3(i) | norm-i-i 27374 norm-i 27370 |
[Beran] p.
97 | Theorem 3.3(ii) | norm-ii-i 27378 norm-ii 27379 normlem0 27350 normlem1 27351 normlem2 27352 normlem3 27353 normlem4 27354 normlem5 27355 normlem6 27356 normlem7 27357 normlem7tALT 27360 |
[Beran] p.
97 | Theorem 3.3(iii) | norm-iii-i 27380 norm-iii 27381 |
[Beran] p.
98 | Remark 3.4 | bcs 27422 bcsiALT 27420 bcsiHIL 27421 |
[Beran] p.
98 | Remark 3.4(B) | normlem9at 27362 normpar 27396 normpari 27395 |
[Beran] p.
98 | Remark 3.4(C) | normpyc 27387 normpyth 27386 normpythi 27383 |
[Beran] p.
99 | Remark | lnfn0 28290 lnfn0i 28285 lnop0 28209 lnop0i 28213 |
[Beran] p.
99 | Theorem 3.5(i) | nmcexi 28269 nmcfnex 28296 nmcfnexi 28294 nmcopex 28272 nmcopexi 28270 |
[Beran] p.
99 | Theorem 3.5(ii) | nmcfnlb 28297 nmcfnlbi 28295 nmcoplb 28273 nmcoplbi 28271 |
[Beran] p.
99 | Theorem 3.5(iii) | lnfncon 28299 lnfnconi 28298 lnopcon 28278 lnopconi 28277 |
[Beran] p.
100 | Lemma 3.6 | normpar2i 27397 |
[Beran] p.
101 | Lemma 3.6 | norm3adifi 27394 norm3adifii 27389 norm3dif 27391 norm3difi 27388 |
[Beran] p.
102 | Theorem 3.7(i) | chocunii 27544 pjhth 27636 pjhtheu 27637 pjpjhth 27668 pjpjhthi 27669 pjth 23018 |
[Beran] p.
102 | Theorem 3.7(ii) | ococ 27649 ococi 27648 |
[Beran] p.
103 | Remark 3.8 | nlelchi 28304 |
[Beran] p.
104 | Theorem 3.9 | riesz3i 28305 riesz4 28307 riesz4i 28306 |
[Beran] p.
104 | Theorem 3.10 | cnlnadj 28322 cnlnadjeu 28321 cnlnadjeui 28320 cnlnadji 28319 cnlnadjlem1 28310 nmopadjlei 28331 |
[Beran] p.
106 | Theorem 3.11(i) | adjeq0 28334 |
[Beran] p.
106 | Theorem 3.11(v) | nmopadji 28333 |
[Beran] p.
106 | Theorem 3.11(ii) | adjmul 28335 |
[Beran] p.
106 | Theorem 3.11(iv) | adjadj 28179 |
[Beran] p.
106 | Theorem 3.11(vi) | nmopcoadj2i 28345 nmopcoadji 28344 |
[Beran] p.
106 | Theorem 3.11(iii) | adjadd 28336 |
[Beran] p.
106 | Theorem 3.11(vii) | nmopcoadj0i 28346 |
[Beran] p.
106 | Theorem 3.11(viii) | adjcoi 28343 pjadj2coi 28447 pjadjcoi 28404 |
[Beran] p.
107 | Definition | df-ch 27462 isch2 27464 |
[Beran] p.
107 | Remark 3.12 | choccl 27549 isch3 27482 occl 27547 ocsh 27526 shoccl 27548 shocsh 27527 |
[Beran] p.
107 | Remark 3.12(B) | ococin 27651 |
[Beran] p.
108 | Theorem 3.13 | chintcl 27575 |
[Beran] p.
109 | Property (i) | pjadj2 28430 pjadj3 28431 pjadji 27928 pjadjii 27917 |
[Beran] p.
109 | Property (ii) | pjidmco 28424 pjidmcoi 28420 pjidmi 27916 |
[Beran] p.
110 | Definition of projector ordering | pjordi 28416 |
[Beran] p.
111 | Remark | ho0val 27993 pjch1 27913 |
[Beran] p.
111 | Definition | df-hfmul 27977 df-hfsum 27976 df-hodif 27975 df-homul 27974 df-hosum 27973 |
[Beran] p.
111 | Lemma 4.4(i) | pjo 27914 |
[Beran] p.
111 | Lemma 4.4(ii) | pjch 27937 pjchi 27675 |
[Beran] p.
111 | Lemma 4.4(iii) | pjoc2 27682 pjoc2i 27681 |
[Beran] p.
112 | Theorem 4.5(i)->(ii) | pjss2i 27923 |
[Beran] p.
112 | Theorem 4.5(i)->(iv) | pjssmi 28408 pjssmii 27924 |
[Beran] p.
112 | Theorem 4.5(i)<->(ii) | pjss2coi 28407 |
[Beran] p.
112 | Theorem 4.5(i)<->(iii) | pjss1coi 28406 |
[Beran] p.
112 | Theorem 4.5(i)<->(vi) | pjnormssi 28411 |
[Beran] p.
112 | Theorem 4.5(iv)->(v) | pjssge0i 28409 pjssge0ii 27925 |
[Beran] p.
112 | Theorem 4.5(v)<->(vi) | pjdifnormi 28410 pjdifnormii 27926 |
[Bobzien] p.
116 | Statement T3 | stoic3 1692 |
[Bobzien] p.
117 | Statement T2 | stoic2a 1690 |
[Bobzien] p.
117 | Statement T4 | stoic4a 1693 |
[Bobzien] p.
117 | Conclusion the contradictory | stoic1a 1688 |
[Bogachev]
p. 16 | Definition 1.5 | df-oms 29681 |
[Bogachev]
p. 17 | Lemma 1.5.4 | omssubadd 29689 |
[Bogachev]
p. 17 | Example 1.5.2 | omsmon 29687 |
[Bogachev]
p. 41 | Definition 1.11.2 | df-carsg 29691 |
[Bogachev]
p. 42 | Theorem 1.11.4 | carsgsiga 29711 |
[Bogachev]
p. 116 | Definition 2.3.1 | df-itgm 29742 df-sitm 29720 |
[Bogachev]
p. 118 | Chapter 2.4.4 | df-itgm 29742 |
[Bogachev]
p. 118 | Definition 2.4.1 | df-sitg 29719 |
[Bollobas] p.
1 | Section I.1 | df-edg 25865 df-edga 25793 isuhgrop 25736 isusgrop 40392 uhgraop 25833 |
[Bollobas]
p. 2 | Section I.1 | df-subgr 40492 uhgrspan1 40527 uhgrspansubgr 40515 |
[Bollobas]
p. 3 | Section I.1 | cusgrsize 40670 df-cusgr 40558 df-nbgr 40554 fusgrmaxsize 40680 |
[Bollobas]
p. 4 | Definition | df-1wlks 40800 df-wlk 26036 df-wlks 40801 |
[Bollobas] p.
5 | Notation | df-pth 26038 df-pths 40923 |
[Bollobas] p.
5 | Definition | df-crct 26040 df-crcts 40992 df-cycl 26041 df-cycls 40993 df-trail 26037 df-trls 40901 df-wlkon 26042 df-wlkson 40802 |
[Bollobas] p.
7 | Section I.1 | df-ushgr 25725 |
[BourbakiAlg1] p. 1 | Definition
1 | df-clintop 41626 df-cllaw 41612 df-mgm 17065 df-mgm2 41645 |
[BourbakiAlg1] p. 4 | Definition
5 | df-assintop 41627 df-asslaw 41614 df-sgrp 17107 df-sgrp2 41647 |
[BourbakiAlg1] p. 7 | Definition
8 | df-cmgm2 41646 df-comlaw 41613 |
[BourbakiAlg1] p.
12 | Definition 2 | df-mnd 17118 |
[BourbakiAlg1] p.
92 | Definition 1 | df-ring 18372 |
[BourbakiAlg1] p. 93 | Section
I.8.1 | df-rng0 41665 |
[BourbakiEns] p.
| Proposition 8 | fcof1 6442 fcofo 6443 |
[BourbakiTop1] p.
| Remark | xnegmnf 11915 xnegpnf 11914 |
[BourbakiTop1] p.
| Remark | rexneg 11916 |
[BourbakiTop1] p.
| Theorem | neiss 20723 |
[BourbakiTop1] p.
| Remark 3 | ust0 21833 ustfilxp 21826 |
[BourbakiTop1] p.
| Axiom GT' | tgpsubcn 21704 |
[BourbakiTop1] p.
| Example 1 | cstucnd 21898 iducn 21897 snfil 21478 |
[BourbakiTop1] p.
| Example 2 | neifil 21494 |
[BourbakiTop1] p.
| Theorem 1 | cnextcn 21681 |
[BourbakiTop1] p.
| Theorem 2 | ucnextcn 21918 |
[BourbakiTop1] p. | Theorem
3 | df-hcmp 29331 |
[BourbakiTop1] p.
| Definition | istgp 21691 |
[BourbakiTop1] p.
| Paragraph 3 | infil 21477 |
[BourbakiTop1] p.
| Proposition | cnpco 20881 ishmeo 21372 neips 20727 |
[BourbakiTop1] p.
| Definition 1 | df-ucn 21890 df-ust 21814 filintn0 21475 ucnprima 21896 |
[BourbakiTop1] p.
| Definition 2 | df-cfilu 21901 |
[BourbakiTop1] p.
| Definition 3 | df-cusp 21912 df-usp 21871 df-utop 21845 trust 21843 |
[BourbakiTop1] p. | Definition
6 | df-pcmp 29251 |
[BourbakiTop1] p.
| Condition F_I | ustssel 21819 |
[BourbakiTop1] p.
| Condition U_I | ustdiag 21822 |
[BourbakiTop1] p.
| Property V_iv | neiptopreu 20747 |
[BourbakiTop1] p.
| Proposition 1 | ucncn 21899 ustund 21835 ustuqtop 21860 |
[BourbakiTop1] p.
| Proposition 2 | neiptopreu 20747 utop2nei 21864 utop3cls 21865 |
[BourbakiTop1] p.
| Proposition 3 | fmucnd 21906 uspreg 21888 utopreg 21866 |
[BourbakiTop1] p.
| Proposition 4 | imasncld 21304 imasncls 21305 imasnopn 21303 |
[BourbakiTop1] p.
| Proposition 9 | cnpflf2 21614 |
[BourbakiTop1] p.
| Theorem 1 (d) | iscncl 20883 |
[BourbakiTop1] p.
| Condition F_II | ustincl 21821 |
[BourbakiTop1] p.
| Condition U_II | ustinvel 21823 |
[BourbakiTop1] p.
| Proposition 11 | cnextucn 21917 |
[BourbakiTop1] p.
| Proposition Vi | ssnei2 20730 |
[BourbakiTop1] p.
| Condition F_IIb | ustbasel 21820 |
[BourbakiTop1] p.
| Condition U_III | ustexhalf 21824 |
[BourbakiTop1] p.
| Definition C''' | df-cmp 21000 |
[BourbakiTop1] p.
| Proposition Vii | innei 20739 |
[BourbakiTop1] p.
| Proposition Viv | neissex 20741 |
[BourbakiTop1] p.
| Proposition Viii | elnei 20725 ssnei 20724 |
[BourbakiTop1] p.
| Remark below def. 1 | filn0 21476 |
[BourbakiTop1] p.
| Axioms FI, FIIa, FIIb, FIII) | df-fil 21460 |
[BourbakiTop1] p.
| Definition is due to Bourbaki (Def. 1 | df-top 20521 |
[BourbakiTop2] p. 195 | Definition
1 | df-ldlf 29248 |
[BrosowskiDeutsh] p. 89 | Proof
follows | stoweidlem62 38955 |
[BrosowskiDeutsh] p. 89 | Lemmas
are written following | stowei 38957 stoweid 38956 |
[BrosowskiDeutsh] p. 90 | Lemma
1 | stoweidlem1 38894 stoweidlem10 38903 stoweidlem14 38907 stoweidlem15 38908 stoweidlem35 38928 stoweidlem36 38929 stoweidlem37 38930 stoweidlem38 38931 stoweidlem40 38933 stoweidlem41 38934 stoweidlem43 38936 stoweidlem44 38937 stoweidlem46 38939 stoweidlem5 38898 stoweidlem50 38943 stoweidlem52 38945 stoweidlem53 38946 stoweidlem55 38948 stoweidlem56 38949 |
[BrosowskiDeutsh] p. 90 | Lemma 1
| stoweidlem23 38916 stoweidlem24 38917 stoweidlem27 38920 stoweidlem28 38921 stoweidlem30 38923 |
[BrosowskiDeutsh] p.
91 | Proof | stoweidlem34 38927 stoweidlem59 38952 stoweidlem60 38953 |
[BrosowskiDeutsh] p. 91 | Lemma
1 | stoweidlem45 38938 stoweidlem49 38942 stoweidlem7 38900 |
[BrosowskiDeutsh] p. 91 | Lemma
2 | stoweidlem31 38924 stoweidlem39 38932 stoweidlem42 38935 stoweidlem48 38941 stoweidlem51 38944 stoweidlem54 38947 stoweidlem57 38950 stoweidlem58 38951 |
[BrosowskiDeutsh] p. 91 | Lemma 1
| stoweidlem25 38918 |
[BrosowskiDeutsh] p. 91 | Lemma
proves that the function ` ` (as defined | stoweidlem17 38910 |
[BrosowskiDeutsh] p.
92 | Proof | stoweidlem11 38904 stoweidlem13 38906 stoweidlem26 38919 stoweidlem61 38954 |
[BrosowskiDeutsh] p. 92 | Lemma
2 | stoweidlem18 38911 |
[Bruck] p.
1 | Section I.1 | df-clintop 41626 df-mgm 17065 df-mgm2 41645 |
[Bruck] p. 23 | Section
II.1 | df-sgrp 17107 df-sgrp2 41647 |
[Bruck] p. 28 | Theorem
3.2 | dfgrp3 17337 |
[ChoquetDD] p.
2 | Definition of mapping | df-mpt 4645 |
[Church] p. 129 | Section
II.24 | df-ifp 1007 dfifp2 1008 |
[Clemente] p.
10 | Definition IT | natded 26652 |
[Clemente] p.
10 | Definition I` `m,n | natded 26652 |
[Clemente] p.
11 | Definition E=>m,n | natded 26652 |
[Clemente] p.
11 | Definition I=>m,n | natded 26652 |
[Clemente] p.
11 | Definition E` `(1) | natded 26652 |
[Clemente] p.
11 | Definition E` `(2) | natded 26652 |
[Clemente] p.
12 | Definition E` `m,n,p | natded 26652 |
[Clemente] p.
12 | Definition I` `n(1) | natded 26652 |
[Clemente] p.
12 | Definition I` `n(2) | natded 26652 |
[Clemente] p.
13 | Definition I` `m,n,p | natded 26652 |
[Clemente] p. 14 | Proof
5.11 | natded 26652 |
[Clemente] p.
14 | Definition E` `n | natded 26652 |
[Clemente] p.
15 | Theorem 5.2 | ex-natded5.2-2 26654 ex-natded5.2 26653 |
[Clemente] p.
16 | Theorem 5.3 | ex-natded5.3-2 26657 ex-natded5.3 26656 |
[Clemente] p.
18 | Theorem 5.5 | ex-natded5.5 26659 |
[Clemente] p.
19 | Theorem 5.7 | ex-natded5.7-2 26661 ex-natded5.7 26660 |
[Clemente] p.
20 | Theorem 5.8 | ex-natded5.8-2 26663 ex-natded5.8 26662 |
[Clemente] p.
20 | Theorem 5.13 | ex-natded5.13-2 26665 ex-natded5.13 26664 |
[Clemente] p.
32 | Definition I` `n | natded 26652 |
[Clemente] p.
32 | Definition E` `m,n,p,a | natded 26652 |
[Clemente] p.
32 | Definition E` `n,t | natded 26652 |
[Clemente] p.
32 | Definition I` `n,t | natded 26652 |
[Clemente] p.
43 | Theorem 9.20 | ex-natded9.20 26666 |
[Clemente] p.
45 | Theorem 9.20 | ex-natded9.20-2 26667 |
[Clemente] p.
45 | Theorem 9.26 | ex-natded9.26-2 26669 ex-natded9.26 26668 |
[Cohen] p.
301 | Remark | relogoprlem 24141 |
[Cohen] p. 301 | Property
2 | relogmul 24142 relogmuld 24175 |
[Cohen] p. 301 | Property
3 | relogdiv 24143 relogdivd 24176 |
[Cohen] p. 301 | Property
4 | relogexp 24146 |
[Cohen] p. 301 | Property
1a | log1 24136 |
[Cohen] p. 301 | Property
1b | loge 24137 |
[Cohen4] p.
348 | Observation | relogbcxpb 24325 |
[Cohen4] p.
349 | Property | relogbf 24329 |
[Cohen4] p.
352 | Definition | elogb 24308 |
[Cohen4] p. 361 | Property
2 | relogbmul 24315 |
[Cohen4] p. 361 | Property
3 | logbrec 24320 relogbdiv 24317 |
[Cohen4] p. 361 | Property
4 | relogbreexp 24313 |
[Cohen4] p. 361 | Property
6 | relogbexp 24318 |
[Cohen4] p. 361 | Property
1(a) | logbid1 24306 |
[Cohen4] p. 361 | Property
1(b) | logb1 24307 |
[Cohen4] p.
367 | Property | logbchbase 24309 |
[Cohen4] p. 377 | Property
2 | logblt 24322 |
[Cohn] p.
4 | Proposition 1.1.5 | sxbrsigalem1 29674 sxbrsigalem4 29676 |
[Cohn] p. 81 | Section
II.5 | acsdomd 17004 acsinfd 17003 acsinfdimd 17005 acsmap2d 17002 acsmapd 17001 |
[Cohn] p.
143 | Example 5.1.1 | sxbrsiga 29679 |
[Connell] p.
57 | Definition | df-scmat 20116 df-scmatalt 41982 |
[CormenLeisersonRivest] p.
33 | Equation 2.4 | fldiv2 12522 |
[Crawley] p.
1 | Definition of poset | df-poset 16769 |
[Crawley] p.
107 | Theorem 13.2 | hlsupr 33690 |
[Crawley] p.
110 | Theorem 13.3 | arglem1N 34495 dalaw 34190 |
[Crawley] p.
111 | Theorem 13.4 | hlathil 36271 |
[Crawley] p.
111 | Definition of set W | df-watsN 34294 |
[Crawley] p.
111 | Definition of dilation | df-dilN 34410 df-ldil 34408 isldil 34414 |
[Crawley] p.
111 | Definition of translation | df-ltrn 34409 df-trnN 34411 isltrn 34423 ltrnu 34425 |
[Crawley] p.
112 | Lemma A | cdlema1N 34095 cdlema2N 34096 exatleN 33708 |
[Crawley] p.
112 | Lemma B | 1cvrat 33780 cdlemb 34098 cdlemb2 34345 cdlemb3 34912 idltrn 34454 l1cvat 33360 lhpat 34347 lhpat2 34349 lshpat 33361 ltrnel 34443 ltrnmw 34455 |
[Crawley] p.
112 | Lemma C | cdlemc1 34496 cdlemc2 34497 ltrnnidn 34479 trlat 34474 trljat1 34471 trljat2 34472 trljat3 34473 trlne 34490 trlnidat 34478 trlnle 34491 |
[Crawley] p.
112 | Definition of automorphism | df-pautN 34295 |
[Crawley] p.
113 | Lemma C | cdlemc 34502 cdlemc3 34498 cdlemc4 34499 |
[Crawley] p.
113 | Lemma D | cdlemd 34512 cdlemd1 34503 cdlemd2 34504 cdlemd3 34505 cdlemd4 34506 cdlemd5 34507 cdlemd6 34508 cdlemd7 34509 cdlemd8 34510 cdlemd9 34511 cdleme31sde 34691 cdleme31se 34688 cdleme31se2 34689 cdleme31snd 34692 cdleme32a 34747 cdleme32b 34748 cdleme32c 34749 cdleme32d 34750 cdleme32e 34751 cdleme32f 34752 cdleme32fva 34743 cdleme32fva1 34744 cdleme32fvcl 34746 cdleme32le 34753 cdleme48fv 34805 cdleme4gfv 34813 cdleme50eq 34847 cdleme50f 34848 cdleme50f1 34849 cdleme50f1o 34852 cdleme50laut 34853 cdleme50ldil 34854 cdleme50lebi 34846 cdleme50rn 34851 cdleme50rnlem 34850 cdlemeg49le 34817 cdlemeg49lebilem 34845 |
[Crawley] p.
113 | Lemma E | cdleme 34866 cdleme00a 34514 cdleme01N 34526 cdleme02N 34527 cdleme0a 34516 cdleme0aa 34515 cdleme0b 34517 cdleme0c 34518 cdleme0cp 34519 cdleme0cq 34520 cdleme0dN 34521 cdleme0e 34522 cdleme0ex1N 34528 cdleme0ex2N 34529 cdleme0fN 34523 cdleme0gN 34524 cdleme0moN 34530 cdleme1 34532 cdleme10 34559 cdleme10tN 34563 cdleme11 34575 cdleme11a 34565 cdleme11c 34566 cdleme11dN 34567 cdleme11e 34568 cdleme11fN 34569 cdleme11g 34570 cdleme11h 34571 cdleme11j 34572 cdleme11k 34573 cdleme11l 34574 cdleme12 34576 cdleme13 34577 cdleme14 34578 cdleme15 34583 cdleme15a 34579 cdleme15b 34580 cdleme15c 34581 cdleme15d 34582 cdleme16 34590 cdleme16aN 34564 cdleme16b 34584 cdleme16c 34585 cdleme16d 34586 cdleme16e 34587 cdleme16f 34588 cdleme16g 34589 cdleme19a 34609 cdleme19b 34610 cdleme19c 34611 cdleme19d 34612 cdleme19e 34613 cdleme19f 34614 cdleme1b 34531 cdleme2 34533 cdleme20aN 34615 cdleme20bN 34616 cdleme20c 34617 cdleme20d 34618 cdleme20e 34619 cdleme20f 34620 cdleme20g 34621 cdleme20h 34622 cdleme20i 34623 cdleme20j 34624 cdleme20k 34625 cdleme20l 34628 cdleme20l1 34626 cdleme20l2 34627 cdleme20m 34629 cdleme20y 34607 cdleme20zN 34606 cdleme21 34643 cdleme21d 34636 cdleme21e 34637 cdleme22a 34646 cdleme22aa 34645 cdleme22b 34647 cdleme22cN 34648 cdleme22d 34649 cdleme22e 34650 cdleme22eALTN 34651 cdleme22f 34652 cdleme22f2 34653 cdleme22g 34654 cdleme23a 34655 cdleme23b 34656 cdleme23c 34657 cdleme26e 34665 cdleme26eALTN 34667 cdleme26ee 34666 cdleme26f 34669 cdleme26f2 34671 cdleme26f2ALTN 34670 cdleme26fALTN 34668 cdleme27N 34675 cdleme27a 34673 cdleme27cl 34672 cdleme28c 34678 cdleme3 34542 cdleme30a 34684 cdleme31fv 34696 cdleme31fv1 34697 cdleme31fv1s 34698 cdleme31fv2 34699 cdleme31id 34700 cdleme31sc 34690 cdleme31sdnN 34693 cdleme31sn 34686 cdleme31sn1 34687 cdleme31sn1c 34694 cdleme31sn2 34695 cdleme31so 34685 cdleme35a 34754 cdleme35b 34756 cdleme35c 34757 cdleme35d 34758 cdleme35e 34759 cdleme35f 34760 cdleme35fnpq 34755 cdleme35g 34761 cdleme35h 34762 cdleme35h2 34763 cdleme35sn2aw 34764 cdleme35sn3a 34765 cdleme36a 34766 cdleme36m 34767 cdleme37m 34768 cdleme38m 34769 cdleme38n 34770 cdleme39a 34771 cdleme39n 34772 cdleme3b 34534 cdleme3c 34535 cdleme3d 34536 cdleme3e 34537 cdleme3fN 34538 cdleme3fa 34541 cdleme3g 34539 cdleme3h 34540 cdleme4 34543 cdleme40m 34773 cdleme40n 34774 cdleme40v 34775 cdleme40w 34776 cdleme41fva11 34783 cdleme41sn3aw 34780 cdleme41sn4aw 34781 cdleme41snaw 34782 cdleme42a 34777 cdleme42b 34784 cdleme42c 34778 cdleme42d 34779 cdleme42e 34785 cdleme42f 34786 cdleme42g 34787 cdleme42h 34788 cdleme42i 34789 cdleme42k 34790 cdleme42ke 34791 cdleme42keg 34792 cdleme42mN 34793 cdleme42mgN 34794 cdleme43aN 34795 cdleme43bN 34796 cdleme43cN 34797 cdleme43dN 34798 cdleme5 34545 cdleme50ex 34865 cdleme50ltrn 34863 cdleme51finvN 34862 cdleme51finvfvN 34861 cdleme51finvtrN 34864 cdleme6 34546 cdleme7 34554 cdleme7a 34548 cdleme7aa 34547 cdleme7b 34549 cdleme7c 34550 cdleme7d 34551 cdleme7e 34552 cdleme7ga 34553 cdleme8 34555 cdleme8tN 34560 cdleme9 34558 cdleme9a 34556 cdleme9b 34557 cdleme9tN 34562 cdleme9taN 34561 cdlemeda 34603 cdlemedb 34602 cdlemednpq 34604 cdlemednuN 34605 cdlemefr27cl 34709 cdlemefr32fva1 34716 cdlemefr32fvaN 34715 cdlemefrs32fva 34706 cdlemefrs32fva1 34707 cdlemefs27cl 34719 cdlemefs32fva1 34729 cdlemefs32fvaN 34728 cdlemesner 34601 cdlemeulpq 34525 |
[Crawley] p.
114 | Lemma E | 4atex 34380 4atexlem7 34379 cdleme0nex 34595 cdleme17a 34591 cdleme17c 34593 cdleme17d 34804 cdleme17d1 34594 cdleme17d2 34801 cdleme18a 34596 cdleme18b 34597 cdleme18c 34598 cdleme18d 34600 cdleme4a 34544 |
[Crawley] p.
115 | Lemma E | cdleme21a 34631 cdleme21at 34634 cdleme21b 34632 cdleme21c 34633 cdleme21ct 34635 cdleme21f 34638 cdleme21g 34639 cdleme21h 34640 cdleme21i 34641 cdleme22gb 34599 |
[Crawley] p.
116 | Lemma F | cdlemf 34869 cdlemf1 34867 cdlemf2 34868 |
[Crawley] p.
116 | Lemma G | cdlemftr1 34873 cdlemg16 34963 cdlemg28 35010 cdlemg28a 34999 cdlemg28b 35009 cdlemg3a 34903 cdlemg42 35035 cdlemg43 35036 cdlemg44 35039 cdlemg44a 35037 cdlemg46 35041 cdlemg47 35042 cdlemg9 34940 ltrnco 35025 ltrncom 35044 tgrpabl 35057 trlco 35033 |
[Crawley] p.
116 | Definition of G | df-tgrp 35049 |
[Crawley] p.
117 | Lemma G | cdlemg17 34983 cdlemg17b 34968 |
[Crawley] p.
117 | Definition of E | df-edring-rN 35062 df-edring 35063 |
[Crawley] p.
117 | Definition of trace-preserving endomorphism | istendo 35066 |
[Crawley] p.
118 | Remark | tendopltp 35086 |
[Crawley] p.
118 | Lemma H | cdlemh 35123 cdlemh1 35121 cdlemh2 35122 |
[Crawley] p.
118 | Lemma I | cdlemi 35126 cdlemi1 35124 cdlemi2 35125 |
[Crawley] p.
118 | Lemma J | cdlemj1 35127 cdlemj2 35128 cdlemj3 35129 tendocan 35130 |
[Crawley] p.
118 | Lemma K | cdlemk 35280 cdlemk1 35137 cdlemk10 35149 cdlemk11 35155 cdlemk11t 35252 cdlemk11ta 35235 cdlemk11tb 35237 cdlemk11tc 35251 cdlemk11u-2N 35195 cdlemk11u 35177 cdlemk12 35156 cdlemk12u-2N 35196 cdlemk12u 35178 cdlemk13-2N 35182 cdlemk13 35158 cdlemk14-2N 35184 cdlemk14 35160 cdlemk15-2N 35185 cdlemk15 35161 cdlemk16-2N 35186 cdlemk16 35163 cdlemk16a 35162 cdlemk17-2N 35187 cdlemk17 35164 cdlemk18-2N 35192 cdlemk18-3N 35206 cdlemk18 35174 cdlemk19-2N 35193 cdlemk19 35175 cdlemk19u 35276 cdlemk1u 35165 cdlemk2 35138 cdlemk20-2N 35198 cdlemk20 35180 cdlemk21-2N 35197 cdlemk21N 35179 cdlemk22-3 35207 cdlemk22 35199 cdlemk23-3 35208 cdlemk24-3 35209 cdlemk25-3 35210 cdlemk26-3 35212 cdlemk26b-3 35211 cdlemk27-3 35213 cdlemk28-3 35214 cdlemk29-3 35217 cdlemk3 35139 cdlemk30 35200 cdlemk31 35202 cdlemk32 35203 cdlemk33N 35215 cdlemk34 35216 cdlemk35 35218 cdlemk36 35219 cdlemk37 35220 cdlemk38 35221 cdlemk39 35222 cdlemk39u 35274 cdlemk4 35140 cdlemk41 35226 cdlemk42 35247 cdlemk42yN 35250 cdlemk43N 35269 cdlemk45 35253 cdlemk46 35254 cdlemk47 35255 cdlemk48 35256 cdlemk49 35257 cdlemk5 35142 cdlemk50 35258 cdlemk51 35259 cdlemk52 35260 cdlemk53 35263 cdlemk54 35264 cdlemk55 35267 cdlemk55u 35272 cdlemk56 35277 cdlemk5a 35141 cdlemk5auN 35166 cdlemk5u 35167 cdlemk6 35143 cdlemk6u 35168 cdlemk7 35154 cdlemk7u-2N 35194 cdlemk7u 35176 cdlemk8 35144 cdlemk9 35145 cdlemk9bN 35146 cdlemki 35147 cdlemkid 35242 cdlemkj-2N 35188 cdlemkj 35169 cdlemksat 35152 cdlemksel 35151 cdlemksv 35150 cdlemksv2 35153 cdlemkuat 35172 cdlemkuel-2N 35190 cdlemkuel-3 35204 cdlemkuel 35171 cdlemkuv-2N 35189 cdlemkuv2-2 35191 cdlemkuv2-3N 35205 cdlemkuv2 35173 cdlemkuvN 35170 cdlemkvcl 35148 cdlemky 35232 cdlemkyyN 35268 tendoex 35281 |
[Crawley] p.
120 | Remark | dva1dim 35291 |
[Crawley] p.
120 | Lemma L | cdleml1N 35282 cdleml2N 35283 cdleml3N 35284 cdleml4N 35285 cdleml5N 35286 cdleml6 35287 cdleml7 35288 cdleml8 35289 cdleml9 35290 dia1dim 35368 |
[Crawley] p.
120 | Lemma M | dia11N 35355 diaf11N 35356 dialss 35353 diaord 35354 dibf11N 35468 djajN 35444 |
[Crawley] p.
120 | Definition of isomorphism map | diaval 35339 |
[Crawley] p.
121 | Lemma M | cdlemm10N 35425 dia2dimlem1 35371 dia2dimlem2 35372 dia2dimlem3 35373 dia2dimlem4 35374 dia2dimlem5 35375 diaf1oN 35437 diarnN 35436 dvheveccl 35419 dvhopN 35423 |
[Crawley] p.
121 | Lemma N | cdlemn 35519 cdlemn10 35513 cdlemn11 35518 cdlemn11a 35514 cdlemn11b 35515 cdlemn11c 35516 cdlemn11pre 35517 cdlemn2 35502 cdlemn2a 35503 cdlemn3 35504 cdlemn4 35505 cdlemn4a 35506 cdlemn5 35508 cdlemn5pre 35507 cdlemn6 35509 cdlemn7 35510 cdlemn8 35511 cdlemn9 35512 diclspsn 35501 |
[Crawley] p.
121 | Definition of phi(q) | df-dic 35480 |
[Crawley] p.
122 | Lemma N | dih11 35572 dihf11 35574 dihjust 35524 dihjustlem 35523 dihord 35571 dihord1 35525 dihord10 35530 dihord11b 35529 dihord11c 35531 dihord2 35534 dihord2a 35526 dihord2b 35527 dihord2cN 35528 dihord2pre 35532 dihord2pre2 35533 dihordlem6 35520 dihordlem7 35521 dihordlem7b 35522 |
[Crawley] p.
122 | Definition of isomorphism map | dihffval 35537 dihfval 35538 dihval 35539 |
[Diestel] p.
3 | Section 1.1 | df-cusgr 40558 df-nbgr 40554 |
[Diestel] p.
4 | Section 1.1 | df-subgr 40492 uhgrspan1 40527 uhgrspansubgr 40515 |
[Diestel] p. 27 | Section
1.10 | df-ushgr 25725 |
[Eisenberg] p.
67 | Definition 5.3 | df-dif 3543 |
[Eisenberg] p.
82 | Definition 6.3 | dfom3 8427 |
[Eisenberg] p.
125 | Definition 8.21 | df-map 7746 |
[Eisenberg] p.
216 | Example 13.2(4) | omenps 8435 |
[Eisenberg] p.
310 | Theorem 19.8 | cardprc 8689 |
[Eisenberg] p.
310 | Corollary 19.7(2) | cardsdom 9256 |
[Enderton] p. 18 | Axiom
of Empty Set | axnul 4716 |
[Enderton] p.
19 | Definition | df-tp 4130 |
[Enderton] p.
26 | Exercise 5 | unissb 4405 |
[Enderton] p.
26 | Exercise 10 | pwel 4847 |
[Enderton] p.
28 | Exercise 7(b) | pwun 4946 |
[Enderton] p.
30 | Theorem "Distributive laws" | iinin1 4527 iinin2 4526 iinun2 4522 iunin1 4521 iunin1f 28757 iunin2 4520 uniin1 28750 uniin2 28751 |
[Enderton] p.
31 | Theorem "De Morgan's laws" | iindif2 4525 iundif2 4523 |
[Enderton] p.
32 | Exercise 20 | unineq 3836 |
[Enderton] p.
33 | Exercise 23 | iinuni 4545 |
[Enderton] p.
33 | Exercise 25 | iununi 4546 |
[Enderton] p.
33 | Exercise 24(a) | iinpw 4550 |
[Enderton] p.
33 | Exercise 24(b) | iunpw 6870 iunpwss 4551 |
[Enderton] p.
36 | Definition | opthwiener 4901 |
[Enderton] p.
38 | Exercise 6(a) | unipw 4845 |
[Enderton] p.
38 | Exercise 6(b) | pwuni 4825 |
[Enderton] p. 41 | Lemma
3D | opeluu 4866 rnex 6992
rnexg 6990 |
[Enderton] p.
41 | Exercise 8 | dmuni 5256 rnuni 5463 |
[Enderton] p.
42 | Definition of a function | dffun7 5830 dffun8 5831 |
[Enderton] p.
43 | Definition of function value | funfv2 6176 |
[Enderton] p.
43 | Definition of single-rooted | funcnv 5872 |
[Enderton] p.
44 | Definition (d) | dfima2 5387 dfima3 5388 |
[Enderton] p.
47 | Theorem 3H | fvco2 6183 |
[Enderton] p. 49 | Axiom
of Choice (first form) | ac7 9178 ac7g 9179
df-ac 8822 dfac2 8836 dfac2a 8835 dfac3 8827 dfac7 8837 |
[Enderton] p.
50 | Theorem 3K(a) | imauni 6408 |
[Enderton] p.
52 | Definition | df-map 7746 |
[Enderton] p.
53 | Exercise 21 | coass 5571 |
[Enderton] p.
53 | Exercise 27 | dmco 5560 |
[Enderton] p.
53 | Exercise 14(a) | funin 5879 |
[Enderton] p.
53 | Exercise 22(a) | imass2 5420 |
[Enderton] p.
54 | Remark | ixpf 7816 ixpssmap 7828 |
[Enderton] p.
54 | Definition of infinite Cartesian product | df-ixp 7795 |
[Enderton] p. 55 | Axiom
of Choice (second form) | ac9 9188 ac9s 9198 |
[Enderton] p.
56 | Theorem 3M | erref 7649 |
[Enderton] p. 57 | Lemma
3N | erthi 7680 |
[Enderton] p.
57 | Definition | df-ec 7631 |
[Enderton] p.
58 | Definition | df-qs 7635 |
[Enderton] p.
61 | Exercise 35 | df-ec 7631 |
[Enderton] p.
65 | Exercise 56(a) | dmun 5253 |
[Enderton] p.
68 | Definition of successor | df-suc 5646 |
[Enderton] p.
71 | Definition | df-tr 4681 dftr4 4685 |
[Enderton] p.
72 | Theorem 4E | unisuc 5718 |
[Enderton] p.
73 | Exercise 6 | unisuc 5718 |
[Enderton] p.
73 | Exercise 5(a) | truni 4695 |
[Enderton] p.
73 | Exercise 5(b) | trint 4696 trintALT 38139 |
[Enderton] p.
79 | Theorem 4I(A1) | nna0 7571 |
[Enderton] p.
79 | Theorem 4I(A2) | nnasuc 7573 onasuc 7495 |
[Enderton] p.
79 | Definition of operation value | df-ov 6552 |
[Enderton] p.
80 | Theorem 4J(A1) | nnm0 7572 |
[Enderton] p.
80 | Theorem 4J(A2) | nnmsuc 7574 onmsuc 7496 |
[Enderton] p.
81 | Theorem 4K(1) | nnaass 7589 |
[Enderton] p.
81 | Theorem 4K(2) | nna0r 7576 nnacom 7584 |
[Enderton] p.
81 | Theorem 4K(3) | nndi 7590 |
[Enderton] p.
81 | Theorem 4K(4) | nnmass 7591 |
[Enderton] p.
81 | Theorem 4K(5) | nnmcom 7593 |
[Enderton] p.
82 | Exercise 16 | nnm0r 7577 nnmsucr 7592 |
[Enderton] p.
88 | Exercise 23 | nnaordex 7605 |
[Enderton] p.
129 | Definition | df-en 7842 |
[Enderton] p.
132 | Theorem 6B(b) | canth 6508 |
[Enderton] p.
133 | Exercise 1 | xpomen 8721 |
[Enderton] p.
133 | Exercise 2 | qnnen 14781 |
[Enderton] p.
134 | Theorem (Pigeonhole Principle) | php 8029 |
[Enderton] p.
135 | Corollary 6C | php3 8031 |
[Enderton] p.
136 | Corollary 6E | nneneq 8028 |
[Enderton] p.
136 | Corollary 6D(a) | pssinf 8055 |
[Enderton] p.
136 | Corollary 6D(b) | ominf 8057 |
[Enderton] p.
137 | Lemma 6F | pssnn 8063 |
[Enderton] p.
138 | Corollary 6G | ssfi 8065 |
[Enderton] p.
139 | Theorem 6H(c) | mapen 8009 |
[Enderton] p.
142 | Theorem 6I(3) | xpcdaen 8888 |
[Enderton] p.
142 | Theorem 6I(4) | mapcdaen 8889 |
[Enderton] p.
143 | Theorem 6J | cda0en 8884 cda1en 8880 |
[Enderton] p.
144 | Exercise 13 | iunfi 8137 unifi 8138 unifi2 8139 |
[Enderton] p.
144 | Corollary 6K | undif2 3996 unfi 8112
unfi2 8114 |
[Enderton] p.
145 | Figure 38 | ffoss 7020 |
[Enderton] p.
145 | Definition | df-dom 7843 |
[Enderton] p.
146 | Example 1 | domen 7854 domeng 7855 |
[Enderton] p.
146 | Example 3 | nndomo 8039 nnsdom 8434 nnsdomg 8104 |
[Enderton] p.
149 | Theorem 6L(a) | cdadom2 8892 |
[Enderton] p.
149 | Theorem 6L(c) | mapdom1 8010 xpdom1 7944 xpdom1g 7942 xpdom2g 7941 |
[Enderton] p.
149 | Theorem 6L(d) | mapdom2 8016 |
[Enderton] p.
151 | Theorem 6M | zorn 9212 zorng 9209 |
[Enderton] p.
151 | Theorem 6M(4) | ac8 9197 dfac5 8834 |
[Enderton] p.
159 | Theorem 6Q | unictb 9276 |
[Enderton] p.
164 | Example | infdif 8914 |
[Enderton] p.
168 | Definition | df-po 4959 |
[Enderton] p.
192 | Theorem 7M(a) | oneli 5752 |
[Enderton] p.
192 | Theorem 7M(b) | ontr1 5688 |
[Enderton] p.
192 | Theorem 7M(c) | onirri 5751 |
[Enderton] p.
193 | Corollary 7N(b) | 0elon 5695 |
[Enderton] p.
193 | Corollary 7N(c) | onsuci 6930 |
[Enderton] p.
193 | Corollary 7N(d) | ssonunii 6879 |
[Enderton] p.
194 | Remark | onprc 6876 |
[Enderton] p.
194 | Exercise 16 | suc11 5748 |
[Enderton] p.
197 | Definition | df-card 8648 |
[Enderton] p.
197 | Theorem 7P | carden 9252 |
[Enderton] p.
200 | Exercise 25 | tfis 6946 |
[Enderton] p.
202 | Lemma 7T | r1tr 8522 |
[Enderton] p.
202 | Definition | df-r1 8510 |
[Enderton] p.
202 | Theorem 7Q | r1val1 8532 |
[Enderton] p.
204 | Theorem 7V(b) | rankval4 8613 |
[Enderton] p.
206 | Theorem 7X(b) | en2lp 8393 |
[Enderton] p.
207 | Exercise 30 | rankpr 8603 rankprb 8597 rankpw 8589 rankpwi 8569 rankuniss 8612 |
[Enderton] p.
207 | Exercise 34 | opthreg 8398 |
[Enderton] p.
208 | Exercise 35 | suc11reg 8399 |
[Enderton] p.
212 | Definition of aleph | alephval3 8816 |
[Enderton] p.
213 | Theorem 8A(a) | alephord2 8782 |
[Enderton] p.
213 | Theorem 8A(b) | cardalephex 8796 |
[Enderton] p.
218 | Theorem Schema 8E | onfununi 7325 |
[Enderton] p.
222 | Definition of kard | karden 8641 kardex 8640 |
[Enderton] p.
238 | Theorem 8R | oeoa 7564 |
[Enderton] p.
238 | Theorem 8S | oeoe 7566 |
[Enderton] p.
240 | Exercise 25 | oarec 7529 |
[Enderton] p.
257 | Definition of cofinality | cflm 8955 |
[FaureFrolicher] p.
57 | Definition 3.1.9 | mreexd 16125 |
[FaureFrolicher] p.
83 | Definition 4.1.1 | df-mri 16071 |
[FaureFrolicher] p.
83 | Proposition 4.1.3 | acsfiindd 17000 mrieqv2d 16122 mrieqvd 16121 |
[FaureFrolicher] p.
84 | Lemma 4.1.5 | mreexmrid 16126 |
[FaureFrolicher] p.
86 | Proposition 4.2.1 | mreexexd 16131 mreexexlem2d 16128 |
[FaureFrolicher] p.
87 | Theorem 4.2.2 | acsexdimd 17006 mreexfidimd 16134 |
[Frege1879]
p. 11 | Statement | df3or2 37079 |
[Frege1879]
p. 12 | Statement | df3an2 37080 dfxor4 37077 dfxor5 37078 |
[Frege1879]
p. 26 | Axiom 1 | ax-frege1 37104 |
[Frege1879]
p. 26 | Axiom 2 | ax-frege2 37105 |
[Frege1879] p.
26 | Proposition 1 | ax-1 6 |
[Frege1879] p.
26 | Proposition 2 | ax-2 7 |
[Frege1879]
p. 29 | Proposition 3 | frege3 37109 |
[Frege1879]
p. 31 | Proposition 4 | frege4 37113 |
[Frege1879]
p. 32 | Proposition 5 | frege5 37114 |
[Frege1879]
p. 33 | Proposition 6 | frege6 37120 |
[Frege1879]
p. 34 | Proposition 7 | frege7 37122 |
[Frege1879]
p. 35 | Axiom 8 | ax-frege8 37123 axfrege8 37121 |
[Frege1879] p.
35 | Proposition 8 | pm2.04 88 wl-pm2.04 32443 |
[Frege1879]
p. 35 | Proposition 9 | frege9 37126 |
[Frege1879]
p. 36 | Proposition 10 | frege10 37134 |
[Frege1879]
p. 36 | Proposition 11 | frege11 37128 |
[Frege1879]
p. 37 | Proposition 12 | frege12 37127 |
[Frege1879]
p. 37 | Proposition 13 | frege13 37136 |
[Frege1879]
p. 37 | Proposition 14 | frege14 37137 |
[Frege1879]
p. 38 | Proposition 15 | frege15 37140 |
[Frege1879]
p. 38 | Proposition 16 | frege16 37130 |
[Frege1879]
p. 39 | Proposition 17 | frege17 37135 |
[Frege1879]
p. 39 | Proposition 18 | frege18 37132 |
[Frege1879]
p. 39 | Proposition 19 | frege19 37138 |
[Frege1879]
p. 40 | Proposition 20 | frege20 37142 |
[Frege1879]
p. 40 | Proposition 21 | frege21 37141 |
[Frege1879]
p. 41 | Proposition 22 | frege22 37133 |
[Frege1879]
p. 42 | Proposition 23 | frege23 37139 |
[Frege1879]
p. 42 | Proposition 24 | frege24 37129 |
[Frege1879]
p. 42 | Proposition 25 | frege25 37131 rp-frege25 37119 |
[Frege1879]
p. 42 | Proposition 26 | frege26 37124 |
[Frege1879]
p. 43 | Axiom 28 | ax-frege28 37144 |
[Frege1879]
p. 43 | Proposition 27 | frege27 37125 |
[Frege1879] p.
43 | Proposition 28 | con3 148 |
[Frege1879]
p. 43 | Proposition 29 | frege29 37145 |
[Frege1879]
p. 44 | Axiom 31 | ax-frege31 37148 axfrege31 37147 |
[Frege1879]
p. 44 | Proposition 30 | frege30 37146 |
[Frege1879] p.
44 | Proposition 31 | notnotr 124 |
[Frege1879]
p. 44 | Proposition 32 | frege32 37149 |
[Frege1879]
p. 44 | Proposition 33 | frege33 37150 |
[Frege1879]
p. 45 | Proposition 34 | frege34 37151 |
[Frege1879]
p. 45 | Proposition 35 | frege35 37152 |
[Frege1879]
p. 45 | Proposition 36 | frege36 37153 |
[Frege1879]
p. 46 | Proposition 37 | frege37 37154 |
[Frege1879]
p. 46 | Proposition 38 | frege38 37155 |
[Frege1879]
p. 46 | Proposition 39 | frege39 37156 |
[Frege1879]
p. 46 | Proposition 40 | frege40 37157 |
[Frege1879]
p. 47 | Axiom 41 | ax-frege41 37159 axfrege41 37158 |
[Frege1879] p.
47 | Proposition 41 | notnot 135 |
[Frege1879]
p. 47 | Proposition 42 | frege42 37160 |
[Frege1879]
p. 47 | Proposition 43 | frege43 37161 |
[Frege1879]
p. 47 | Proposition 44 | frege44 37162 |
[Frege1879]
p. 47 | Proposition 45 | frege45 37163 |
[Frege1879]
p. 48 | Proposition 46 | frege46 37164 |
[Frege1879]
p. 48 | Proposition 47 | frege47 37165 |
[Frege1879]
p. 49 | Proposition 48 | frege48 37166 |
[Frege1879]
p. 49 | Proposition 49 | frege49 37167 |
[Frege1879]
p. 49 | Proposition 50 | frege50 37168 |
[Frege1879]
p. 50 | Axiom 52 | ax-frege52a 37171 ax-frege52c 37202 frege52aid 37172 frege52b 37203 |
[Frege1879]
p. 50 | Axiom 54 | ax-frege54a 37176 ax-frege54c 37206 frege54b 37207 |
[Frege1879]
p. 50 | Proposition 51 | frege51 37169 |
[Frege1879] p.
50 | Proposition 52 | dfsbcq 3404 |
[Frege1879]
p. 50 | Proposition 53 | frege53a 37174 frege53aid 37173 frege53b 37204 frege53c 37228 |
[Frege1879] p.
50 | Proposition 54 | biid 250 eqid 2610 |
[Frege1879]
p. 50 | Proposition 55 | frege55a 37182 frege55aid 37179 frege55b 37211 frege55c 37232 frege55cor1a 37183 frege55lem2a 37181 frege55lem2b 37210 frege55lem2c 37231 |
[Frege1879]
p. 50 | Proposition 56 | frege56a 37185 frege56aid 37184 frege56b 37212 frege56c 37233 |
[Frege1879]
p. 51 | Axiom 58 | ax-frege58a 37189 ax-frege58b 37215 frege58bid 37216 frege58c 37235 |
[Frege1879]
p. 51 | Proposition 57 | frege57a 37187 frege57aid 37186 frege57b 37213 frege57c 37234 |
[Frege1879] p.
51 | Proposition 58 | spsbc 3415 |
[Frege1879]
p. 51 | Proposition 59 | frege59a 37191 frege59b 37218 frege59c 37236 |
[Frege1879]
p. 52 | Proposition 60 | frege60a 37192 frege60b 37219 frege60c 37237 |
[Frege1879]
p. 52 | Proposition 61 | frege61a 37193 frege61b 37220 frege61c 37238 |
[Frege1879]
p. 52 | Proposition 62 | frege62a 37194 frege62b 37221 frege62c 37239 |
[Frege1879]
p. 52 | Proposition 63 | frege63a 37195 frege63b 37222 frege63c 37240 |
[Frege1879]
p. 53 | Proposition 64 | frege64a 37196 frege64b 37223 frege64c 37241 |
[Frege1879]
p. 53 | Proposition 65 | frege65a 37197 frege65b 37224 frege65c 37242 |
[Frege1879]
p. 54 | Proposition 66 | frege66a 37198 frege66b 37225 frege66c 37243 |
[Frege1879]
p. 54 | Proposition 67 | frege67a 37199 frege67b 37226 frege67c 37244 |
[Frege1879]
p. 54 | Proposition 68 | frege68a 37200 frege68b 37227 frege68c 37245 |
[Frege1879]
p. 55 | Definition 69 | dffrege69 37246 |
[Frege1879]
p. 58 | Proposition 70 | frege70 37247 |
[Frege1879]
p. 59 | Proposition 71 | frege71 37248 |
[Frege1879]
p. 59 | Proposition 72 | frege72 37249 |
[Frege1879]
p. 59 | Proposition 73 | frege73 37250 |
[Frege1879]
p. 60 | Definition 76 | dffrege76 37253 |
[Frege1879]
p. 60 | Proposition 74 | frege74 37251 |
[Frege1879]
p. 60 | Proposition 75 | frege75 37252 |
[Frege1879]
p. 62 | Proposition 77 | frege77 37254 frege77d 37057 |
[Frege1879]
p. 63 | Proposition 78 | frege78 37255 |
[Frege1879]
p. 63 | Proposition 79 | frege79 37256 |
[Frege1879]
p. 63 | Proposition 80 | frege80 37257 |
[Frege1879]
p. 63 | Proposition 81 | frege81 37258 frege81d 37058 |
[Frege1879]
p. 64 | Proposition 82 | frege82 37259 |
[Frege1879]
p. 65 | Proposition 83 | frege83 37260 frege83d 37059 |
[Frege1879]
p. 65 | Proposition 84 | frege84 37261 |
[Frege1879]
p. 66 | Proposition 85 | frege85 37262 |
[Frege1879]
p. 66 | Proposition 86 | frege86 37263 |
[Frege1879]
p. 66 | Proposition 87 | frege87 37264 frege87d 37061 |
[Frege1879]
p. 67 | Proposition 88 | frege88 37265 |
[Frege1879]
p. 68 | Proposition 89 | frege89 37266 |
[Frege1879]
p. 68 | Proposition 90 | frege90 37267 |
[Frege1879]
p. 68 | Proposition 91 | frege91 37268 frege91d 37062 |
[Frege1879]
p. 69 | Proposition 92 | frege92 37269 |
[Frege1879]
p. 70 | Proposition 93 | frege93 37270 |
[Frege1879]
p. 70 | Proposition 94 | frege94 37271 |
[Frege1879]
p. 70 | Proposition 95 | frege95 37272 |
[Frege1879]
p. 71 | Definition 99 | dffrege99 37276 |
[Frege1879]
p. 71 | Proposition 96 | frege96 37273 frege96d 37060 |
[Frege1879]
p. 71 | Proposition 97 | frege97 37274 frege97d 37063 |
[Frege1879]
p. 71 | Proposition 98 | frege98 37275 frege98d 37064 |
[Frege1879]
p. 72 | Proposition 100 | frege100 37277 |
[Frege1879]
p. 72 | Proposition 101 | frege101 37278 |
[Frege1879]
p. 72 | Proposition 102 | frege102 37279 frege102d 37065 |
[Frege1879]
p. 73 | Proposition 103 | frege103 37280 |
[Frege1879]
p. 73 | Proposition 104 | frege104 37281 |
[Frege1879]
p. 73 | Proposition 105 | frege105 37282 |
[Frege1879]
p. 73 | Proposition 106 | frege106 37283 frege106d 37066 |
[Frege1879]
p. 74 | Proposition 107 | frege107 37284 |
[Frege1879]
p. 74 | Proposition 108 | frege108 37285 frege108d 37067 |
[Frege1879]
p. 74 | Proposition 109 | frege109 37286 frege109d 37068 |
[Frege1879]
p. 75 | Proposition 110 | frege110 37287 |
[Frege1879]
p. 75 | Proposition 111 | frege111 37288 frege111d 37070 |
[Frege1879]
p. 76 | Proposition 112 | frege112 37289 |
[Frege1879]
p. 76 | Proposition 113 | frege113 37290 |
[Frege1879]
p. 76 | Proposition 114 | frege114 37291 frege114d 37069 |
[Frege1879]
p. 77 | Definition 115 | dffrege115 37292 |
[Frege1879]
p. 77 | Proposition 116 | frege116 37293 |
[Frege1879]
p. 78 | Proposition 117 | frege117 37294 |
[Frege1879]
p. 78 | Proposition 118 | frege118 37295 |
[Frege1879]
p. 78 | Proposition 119 | frege119 37296 |
[Frege1879]
p. 78 | Proposition 120 | frege120 37297 |
[Frege1879]
p. 79 | Proposition 121 | frege121 37298 |
[Frege1879]
p. 79 | Proposition 122 | frege122 37299 frege122d 37071 |
[Frege1879]
p. 79 | Proposition 123 | frege123 37300 |
[Frege1879]
p. 80 | Proposition 124 | frege124 37301 frege124d 37072 |
[Frege1879]
p. 81 | Proposition 125 | frege125 37302 |
[Frege1879]
p. 81 | Proposition 126 | frege126 37303 frege126d 37073 |
[Frege1879]
p. 82 | Proposition 127 | frege127 37304 |
[Frege1879]
p. 83 | Proposition 128 | frege128 37305 |
[Frege1879]
p. 83 | Proposition 129 | frege129 37306 frege129d 37074 |
[Frege1879]
p. 84 | Proposition 130 | frege130 37307 |
[Frege1879]
p. 85 | Proposition 131 | frege131 37308 frege131d 37075 |
[Frege1879]
p. 86 | Proposition 132 | frege132 37309 |
[Frege1879]
p. 86 | Proposition 133 | frege133 37310 frege133d 37076 |
[Fremlin1]
p. 13 | Definition 111G (b) | df-salgen 39209 |
[Fremlin1]
p. 13 | Definition 111G (d) | borelmbl 39526 |
[Fremlin1]
p. 13 | Proposition 111G (b) | salgenss 39230 |
[Fremlin1]
p. 14 | Definition 112A | ismea 39344 |
[Fremlin1]
p. 15 | Remark 112B (d) | psmeasure 39364 |
[Fremlin1]
p. 15 | Property 112C (a) | meadjun 39355 meadjunre 39369 |
[Fremlin1]
p. 15 | Property 112C (b) | meassle 39356 |
[Fremlin1]
p. 15 | Property 112C (c) | meaunle 39357 |
[Fremlin1]
p. 16 | Property 112C (d) | iundjiun 39353 meaiunle 39362 meaiunlelem 39361 |
[Fremlin1]
p. 16 | Proposition 112C (e) | meaiuninc 39374 meaiuninc2 39375 meaiuninclem 39373 |
[Fremlin1]
p. 16 | Proposition 112C (f) | meaiininc 39377 meaiininc2 39378 meaiininclem 39376 |
[Fremlin1]
p. 19 | Theorem 113C | caragen0 39396 caragendifcl 39404 caratheodory 39418 omelesplit 39408 |
[Fremlin1]
p. 19 | Definition 113A | isome 39384 isomennd 39421 isomenndlem 39420 |
[Fremlin1]
p. 19 | Remark 113B (c) | omeunle 39406 |
[Fremlin1]
p. 19 | Definition 112Df | caragencmpl 39425 voncmpl 39511 |
[Fremlin1]
p. 19 | Definition 113A (ii) | omessle 39388 |
[Fremlin1]
p. 20 | Theorem 113C | carageniuncl 39413 carageniuncllem1 39411 carageniuncllem2 39412 caragenuncl 39403 caragenuncllem 39402 caragenunicl 39414 |
[Fremlin1]
p. 21 | Remark 113D | caragenel2d 39422 |
[Fremlin1]
p. 21 | Theorem 113C | caratheodorylem1 39416 caratheodorylem2 39417 |
[Fremlin1]
p. 21 | Exercise 113Xa | caragencmpl 39425 |
[Fremlin1]
p. 23 | Lemma 114B | hoidmv1le 39484 hoidmv1lelem1 39481 hoidmv1lelem2 39482 hoidmv1lelem3 39483 |
[Fremlin1]
p. 25 | Definition 114E | isvonmbl 39528 |
[Fremlin1]
p. 29 | Lemma 115B | hoidmv1le 39484 hoidmvle 39490 hoidmvlelem1 39485 hoidmvlelem2 39486 hoidmvlelem3 39487 hoidmvlelem4 39488 hoidmvlelem5 39489 hsphoidmvle2 39475 hsphoif 39466 hsphoival 39469 |
[Fremlin1]
p. 29 | Definition 1135 (b) | hoicvr 39438 |
[Fremlin1]
p. 29 | Definition 115A (b) | hoicvrrex 39446 |
[Fremlin1]
p. 29 | Definition 115A (c) | hoidmv0val 39473 hoidmvn0val 39474 hoidmvval 39467 hoidmvval0 39477 hoidmvval0b 39480 |
[Fremlin1]
p. 30 | Lemma 115B | hoiprodp1 39478 hsphoidmvle 39476 |
[Fremlin1]
p. 30 | Definition 115C | df-ovoln 39427 df-voln 39429 |
[Fremlin1]
p. 30 | Proposition 115D (a) | dmovn 39494 ovn0 39456 ovn0lem 39455 ovnf 39453 ovnome 39463 ovnssle 39451 ovnsslelem 39450 ovnsupge0 39447 |
[Fremlin1]
p. 30 | Proposition 115D (b) | ovnhoi 39493 ovnhoilem1 39491 ovnhoilem2 39492 vonhoi 39557 |
[Fremlin1]
p. 31 | Lemma 115F | hoidifhspdmvle 39510 hoidifhspf 39508 hoidifhspval 39498 hoidifhspval2 39505 hoidifhspval3 39509 hspmbl 39519 hspmbllem1 39516 hspmbllem2 39517 hspmbllem3 39518 |
[Fremlin1]
p. 31 | Definition 115E | voncmpl 39511 vonmea 39464 |
[Fremlin1]
p. 31 | Proposition 115D (a)(iv) | ovnsubadd 39462 ovnsubadd2 39536 ovnsubadd2lem 39535 ovnsubaddlem1 39460 ovnsubaddlem2 39461 |
[Fremlin1]
p. 32 | Proposition 115G (a) | hoimbl 39521 hoimbl2 39555 hoimbllem 39520 hspdifhsp 39506 opnvonmbl 39524 opnvonmbllem2 39523 |
[Fremlin1]
p. 32 | Proposition 115G (b) | borelmbl 39526 |
[Fremlin1]
p. 32 | Proposition 115G (c) | iccvonmbl 39570 iccvonmbllem 39569 ioovonmbl 39568 |
[Fremlin1]
p. 32 | Proposition 115G (d) | vonicc 39576 vonicclem2 39575 vonioo 39573 vonioolem2 39572 vonn0icc 39579 vonn0icc2 39583 vonn0ioo 39578 vonn0ioo2 39581 |
[Fremlin1]
p. 32 | Proposition 115G (e) | ctvonmbl 39580 snvonmbl 39577 vonct 39584 vonsn 39582 |
[Fremlin1]
p. 35 | Lemma 121A | subsalsal 39253 |
[Fremlin1]
p. 35 | Lemma 121A (iii) | subsaliuncl 39252 subsaliuncllem 39251 |
[Fremlin1]
p. 35 | Proposition 121B | salpreimagtge 39611 salpreimalegt 39597 salpreimaltle 39612 |
[Fremlin1]
p. 35 | Proposition 121B (i) | issmf 39614 issmff 39620 issmflem 39613 |
[Fremlin1]
p. 35 | Proposition 121B (ii) | issmfle 39632 issmflelem 39631 issmfltle 39622 |
[Fremlin1]
p. 35 | Proposition 121B (iii) | issmfgt 39643 issmfgtlem 39642 |
[Fremlin1]
p. 36 | Definition 121C | df-smblfn 39587 issmf 39614 issmff 39620 issmfge 39656 issmfgelem 39655 issmfgt 39643 issmfgtlem 39642 issmfle 39632 issmflelem 39631 issmflem 39613 |
[Fremlin1]
p. 36 | Proposition 121B | salpreimagelt 39595 salpreimagtlt 39616 salpreimalelt 39615 |
[Fremlin1]
p. 36 | Proposition 121B (iv) | issmfge 39656 issmfgelem 39655 |
[Fremlin1]
p. 36 | Proposition 121D (a) | bormflebmf 39640 |
[Fremlin1]
p. 36 | Proposition 121D (b) | cnfrrnsmf 39638 cnfsmf 39627 |
[Fremlin1]
p. 36 | Proposition 121D (c) | decsmf 39653 decsmflem 39652 incsmf 39629 incsmflem 39628 |
[Fremlin1]
p. 37 | Proposition 121E (a) | pimconstlt0 39591 pimconstlt1 39592 smfconst 39636 |
[Fremlin1]
p. 37 | Proposition 121E (b) | smfadd 39651 smfaddlem1 39649 smfaddlem2 39650 |
[Fremlin1]
p. 37 | Proposition 121E (c) | smfmulc1 39681 |
[Fremlin1]
p. 37 | Proposition 121E (d) | smfmul 39680 smfmullem1 39676 smfmullem2 39677 smfmullem3 39678 smfmullem4 39679 |
[Fremlin1]
p. 37 | Proposition 121E (e) | smfdiv 39682 |
[Fremlin1]
p. 37 | Proposition 121E (f) | smfpimbor1 39685 smfpimbor1lem2 39684 |
[Fremlin1]
p. 37 | Proposition 121E (g) | smfco 39687 |
[Fremlin1]
p. 37 | Proposition 121E (h) | smfres 39675 |
[Fremlin1]
p. 38 | Proposition 121E (e) | smfrec 39674 |
[Fremlin1]
p. 38 | Proposition 121E (f) | smfpimbor1lem1 39683 smfresal 39673 |
[Fremlin1]
p. 38 | Proposition 121F (a) | smflim 39663 smflimlem1 39657 smflimlem2 39658 smflimlem3 39659 smflimlem4 39660 smflimlem5 39661 smflimlem6 39662 |
[Fremlin1]
p. 39 | Remark 121G | smflim 39663 |
[Fremlin1]
p. 80 | Definition 135E (b) | df-smblfn 39587 |
[Fremlin5] p.
193 | Proposition 563Gb | nulmbl2 23111 |
[Fremlin5] p.
213 | Lemma 565Ca | uniioovol 23153 |
[Fremlin5] p.
214 | Lemma 565Ca | uniioombl 23163 |
[Fremlin5]
p. 218 | Lemma 565Ib | ftc1anclem6 32660 |
[Fremlin5]
p. 220 | Theorem 565Ma | ftc1anc 32663 |
[FreydScedrov] p.
283 | Axiom of Infinity | ax-inf 8418 inf1 8402
inf2 8403 |
[Gleason] p.
117 | Proposition 9-2.1 | df-enq 9612 enqer 9622 |
[Gleason] p.
117 | Proposition 9-2.2 | df-1nq 9617 df-nq 9613 |
[Gleason] p.
117 | Proposition 9-2.3 | df-plpq 9609 df-plq 9615 |
[Gleason] p.
119 | Proposition 9-2.4 | caovmo 6769 df-mpq 9610 df-mq 9616 |
[Gleason] p.
119 | Proposition 9-2.5 | df-rq 9618 |
[Gleason] p.
119 | Proposition 9-2.6 | ltexnq 9676 |
[Gleason] p.
120 | Proposition 9-2.6(i) | halfnq 9677 ltbtwnnq 9679 |
[Gleason] p.
120 | Proposition 9-2.6(ii) | ltanq 9672 |
[Gleason] p.
120 | Proposition 9-2.6(iii) | ltmnq 9673 |
[Gleason] p.
120 | Proposition 9-2.6(iv) | ltrnq 9680 |
[Gleason] p.
121 | Definition 9-3.1 | df-np 9682 |
[Gleason] p.
121 | Definition 9-3.1 (ii) | prcdnq 9694 |
[Gleason] p.
121 | Definition 9-3.1(iii) | prnmax 9696 |
[Gleason] p.
122 | Definition | df-1p 9683 |
[Gleason] p. 122 | Remark
(1) | prub 9695 |
[Gleason] p. 122 | Lemma
9-3.4 | prlem934 9734 |
[Gleason] p.
122 | Proposition 9-3.2 | df-ltp 9686 |
[Gleason] p.
122 | Proposition 9-3.3 | ltsopr 9733 psslinpr 9732 supexpr 9755 suplem1pr 9753 suplem2pr 9754 |
[Gleason] p.
123 | Proposition 9-3.5 | addclpr 9719 addclprlem1 9717 addclprlem2 9718 df-plp 9684 |
[Gleason] p.
123 | Proposition 9-3.5(i) | addasspr 9723 |
[Gleason] p.
123 | Proposition 9-3.5(ii) | addcompr 9722 |
[Gleason] p.
123 | Proposition 9-3.5(iii) | ltaddpr 9735 |
[Gleason] p.
123 | Proposition 9-3.5(iv) | ltexpri 9744 ltexprlem1 9737 ltexprlem2 9738 ltexprlem3 9739 ltexprlem4 9740 ltexprlem5 9741 ltexprlem6 9742 ltexprlem7 9743 |
[Gleason] p.
123 | Proposition 9-3.5(v) | ltapr 9746 ltaprlem 9745 |
[Gleason] p.
123 | Proposition 9-3.5(vi) | addcanpr 9747 |
[Gleason] p. 124 | Lemma
9-3.6 | prlem936 9748 |
[Gleason] p.
124 | Proposition 9-3.7 | df-mp 9685 mulclpr 9721 mulclprlem 9720 reclem2pr 9749 |
[Gleason] p.
124 | Theorem 9-3.7(iv) | 1idpr 9730 |
[Gleason] p.
124 | Proposition 9-3.7(i) | mulasspr 9725 |
[Gleason] p.
124 | Proposition 9-3.7(ii) | mulcompr 9724 |
[Gleason] p.
124 | Proposition 9-3.7(iii) | distrpr 9729 |
[Gleason] p.
124 | Proposition 9-3.7(v) | recexpr 9752 reclem3pr 9750 reclem4pr 9751 |
[Gleason] p.
126 | Proposition 9-4.1 | df-enr 9756 enrer 9765 |
[Gleason] p.
126 | Proposition 9-4.2 | df-0r 9761 df-1r 9762 df-nr 9757 |
[Gleason] p.
126 | Proposition 9-4.3 | df-mr 9759 df-plr 9758 negexsr 9802 recexsr 9807 recexsrlem 9803 |
[Gleason] p.
127 | Proposition 9-4.4 | df-ltr 9760 |
[Gleason] p.
130 | Proposition 10-1.3 | creui 10892 creur 10891 cru 10889 |
[Gleason] p.
130 | Definition 10-1.1(v) | ax-cnre 9888 axcnre 9864 |
[Gleason] p.
132 | Definition 10-3.1 | crim 13703 crimd 13820 crimi 13781 crre 13702 crred 13819 crrei 13780 |
[Gleason] p.
132 | Definition 10-3.2 | remim 13705 remimd 13786 |
[Gleason] p.
133 | Definition 10.36 | absval2 13872 absval2d 14032 absval2i 13984 |
[Gleason] p.
133 | Proposition 10-3.4(a) | cjadd 13729 cjaddd 13808 cjaddi 13776 |
[Gleason] p.
133 | Proposition 10-3.4(c) | cjmul 13730 cjmuld 13809 cjmuli 13777 |
[Gleason] p.
133 | Proposition 10-3.4(e) | cjcj 13728 cjcjd 13787 cjcji 13759 |
[Gleason] p.
133 | Proposition 10-3.4(f) | cjre 13727 cjreb 13711 cjrebd 13790 cjrebi 13762 cjred 13814 rere 13710 rereb 13708 rerebd 13789 rerebi 13761 rered 13812 |
[Gleason] p.
133 | Proposition 10-3.4(h) | addcj 13736 addcjd 13800 addcji 13771 |
[Gleason] p.
133 | Proposition 10-3.7(a) | absval 13826 |
[Gleason] p.
133 | Proposition 10-3.7(b) | abscj 13867 abscjd 14037 abscji 13988 |
[Gleason] p.
133 | Proposition 10-3.7(c) | abs00 13877 abs00d 14033 abs00i 13985 absne0d 14034 |
[Gleason] p.
133 | Proposition 10-3.7(d) | releabs 13909 releabsd 14038 releabsi 13989 |
[Gleason] p.
133 | Proposition 10-3.7(f) | absmul 13882 absmuld 14041 absmuli 13991 |
[Gleason] p.
133 | Proposition 10-3.7(g) | sqabsadd 13870 sqabsaddi 13992 |
[Gleason] p.
133 | Proposition 10-3.7(h) | abstri 13918 abstrid 14043 abstrii 13995 |
[Gleason] p.
134 | Definition 10-4.1 | 0exp0e1 12727 df-exp 12723 exp0 12726 expp1 12729 expp1d 12871 |
[Gleason] p.
135 | Proposition 10-4.2(a) | cxpadd 24225 cxpaddd 24263 expadd 12764 expaddd 12872 expaddz 12766 |
[Gleason] p.
135 | Proposition 10-4.2(b) | cxpmul 24234 cxpmuld 24280 expmul 12767 expmuld 12873 expmulz 12768 |
[Gleason] p.
135 | Proposition 10-4.2(c) | mulcxp 24231 mulcxpd 24274 mulexp 12761 mulexpd 12885 mulexpz 12762 |
[Gleason] p.
140 | Exercise 1 | znnen 14780 |
[Gleason] p.
141 | Definition 11-2.1 | fzval 12199 |
[Gleason] p.
168 | Proposition 12-2.1(a) | climadd 14210 rlimadd 14221 rlimdiv 14224 |
[Gleason] p.
168 | Proposition 12-2.1(b) | climsub 14212 rlimsub 14222 |
[Gleason] p.
168 | Proposition 12-2.1(c) | climmul 14211 rlimmul 14223 |
[Gleason] p.
171 | Corollary 12-2.2 | climmulc2 14215 |
[Gleason] p.
172 | Corollary 12-2.5 | climrecl 14162 |
[Gleason] p.
172 | Proposition 12-2.4(c) | climabs 14182 climcj 14183 climim 14185 climre 14184 rlimabs 14187 rlimcj 14188 rlimim 14190 rlimre 14189 |
[Gleason] p.
173 | Definition 12-3.1 | df-ltxr 9958 df-xr 9957 ltxr 11825 |
[Gleason] p.
175 | Definition 12-4.1 | df-limsup 14050 limsupval 14053 |
[Gleason] p.
180 | Theorem 12-5.1 | climsup 14248 |
[Gleason] p.
180 | Theorem 12-5.3 | caucvg 14257 caucvgb 14258 caucvgr 14254 climcau 14249 |
[Gleason] p.
182 | Exercise 3 | cvgcmp 14389 |
[Gleason] p.
182 | Exercise 4 | cvgrat 14454 |
[Gleason] p.
195 | Theorem 13-2.12 | abs1m 13923 |
[Gleason] p. 217 | Lemma
13-4.1 | btwnzge0 12491 |
[Gleason] p.
223 | Definition 14-1.1 | df-met 19561 |
[Gleason] p.
223 | Definition 14-1.1(a) | met0 21958 xmet0 21957 |
[Gleason] p.
223 | Definition 14-1.1(b) | metgt0 21974 |
[Gleason] p.
223 | Definition 14-1.1(c) | metsym 21965 |
[Gleason] p.
223 | Definition 14-1.1(d) | mettri 21967 mstri 22084 xmettri 21966 xmstri 22083 |
[Gleason] p.
225 | Definition 14-1.5 | xpsmet 21997 |
[Gleason] p.
230 | Proposition 14-2.6 | txlm 21261 |
[Gleason] p.
240 | Theorem 14-4.3 | metcnp4 22916 |
[Gleason] p.
240 | Proposition 14-4.2 | metcnp3 22155 |
[Gleason] p.
243 | Proposition 14-4.16 | addcn 22476 addcn2 14172 mulcn 22478 mulcn2 14174 subcn 22477 subcn2 14173 |
[Gleason] p.
295 | Remark | bcval3 12955 bcval4 12956 |
[Gleason] p.
295 | Equation 2 | bcpasc 12970 |
[Gleason] p.
295 | Definition of binomial coefficient | bcval 12953 df-bc 12952 |
[Gleason] p.
296 | Remark | bcn0 12959 bcnn 12961 |
[Gleason] p.
296 | Theorem 15-2.8 | binom 14401 |
[Gleason] p.
308 | Equation 2 | ef0 14660 |
[Gleason] p.
308 | Equation 3 | efcj 14661 |
[Gleason] p.
309 | Corollary 15-4.3 | efne0 14666 |
[Gleason] p.
309 | Corollary 15-4.4 | efexp 14670 |
[Gleason] p.
310 | Equation 14 | sinadd 14733 |
[Gleason] p.
310 | Equation 15 | cosadd 14734 |
[Gleason] p.
311 | Equation 17 | sincossq 14745 |
[Gleason] p.
311 | Equation 18 | cosbnd 14750 sinbnd 14749 |
[Gleason] p. 311 | Lemma
15-4.7 | sqeqor 12840 sqeqori 12838 |
[Gleason] p.
311 | Definition of pi | df-pi 14642 |
[Godowski]
p. 730 | Equation SF | goeqi 28516 |
[GodowskiGreechie] p.
249 | Equation IV | 3oai 27911 |
[Golan] p.
1 | Remark | srgisid 18351 |
[Golan] p.
1 | Definition | df-srg 18329 |
[Golan] p.
149 | Definition | df-slmd 29085 |
[GramKnuthPat], p. 47 | Definition
2.42 | df-fwddif 31436 |
[Gratzer] p. 23 | Section
0.6 | df-mre 16069 |
[Gratzer] p. 27 | Section
0.6 | df-mri 16071 |
[Hall] p.
1 | Section 1.1 | df-asslaw 41614 df-cllaw 41612 df-comlaw 41613 |
[Hall] p.
2 | Section 1.2 | df-clintop 41626 |
[Hall] p.
7 | Section 1.3 | df-sgrp2 41647 |
[Halmos] p.
31 | Theorem 17.3 | riesz1 28308 riesz2 28309 |
[Halmos] p.
41 | Definition of Hermitian | hmopadj2 28184 |
[Halmos] p.
42 | Definition of projector ordering | pjordi 28416 |
[Halmos] p.
43 | Theorem 26.1 | elpjhmop 28428 elpjidm 28427 pjnmopi 28391 |
[Halmos] p.
44 | Remark | pjinormi 27930 pjinormii 27919 |
[Halmos] p.
44 | Theorem 26.2 | elpjch 28432 pjrn 27950 pjrni 27945 pjvec 27939 |
[Halmos] p.
44 | Theorem 26.3 | pjnorm2 27970 |
[Halmos] p.
44 | Theorem 26.4 | hmopidmpj 28397 hmopidmpji 28395 |
[Halmos] p.
45 | Theorem 27.1 | pjinvari 28434 |
[Halmos] p.
45 | Theorem 27.3 | pjoci 28423 pjocvec 27940 |
[Halmos] p.
45 | Theorem 27.4 | pjorthcoi 28412 |
[Halmos] p.
48 | Theorem 29.2 | pjssposi 28415 |
[Halmos] p.
48 | Theorem 29.3 | pjssdif1i 28418 pjssdif2i 28417 |
[Halmos] p.
50 | Definition of spectrum | df-spec 28098 |
[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 1713 |
[Hatcher] p.
25 | Definition | df-phtpc 22599 df-phtpy 22578 |
[Hatcher] p.
26 | Definition | df-pco 22613 df-pi1 22616 |
[Hatcher] p.
26 | Proposition 1.2 | phtpcer 22602 |
[Hatcher] p.
26 | Proposition 1.3 | pi1grp 22658 |
[Hefferon] p.
240 | Definition 3.12 | df-dmat 20115 df-dmatalt 41981 |
[Helfgott]
p. 2 | Theorem | tgoldbach 40232 |
[Helfgott]
p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 40218 |
[Helfgott]
p. 4 | Section 1.2.2 | ax-hgprmladder 40228 bgoldbtbnd 40225 bgoldbtbnd 40225 tgblthelfgott 40229 |
[Helfgott]
p. 70 | Section 7.4 | ax-tgoldbachgt 40231 |
[Herstein] p.
54 | Exercise 28 | df-grpo 26731 |
[Herstein] p. 55 | Lemma
2.2.1(a) | grpideu 17256 grpoideu 26747 mndideu 17127 |
[Herstein] p. 55 | Lemma
2.2.1(b) | grpinveu 17279 grpoinveu 26757 |
[Herstein] p. 55 | Lemma
2.2.1(c) | grpinvinv 17305 grpo2inv 26769 |
[Herstein] p. 55 | Lemma
2.2.1(d) | grpinvadd 17316 grpoinvop 26771 |
[Herstein] p.
57 | Exercise 1 | dfgrp3e 17338 |
[Hitchcock] p. 5 | Rule
A3 | mptnan 1684 |
[Hitchcock] p. 5 | Rule
A4 | mptxor 1685 |
[Hitchcock] p. 5 | Rule
A5 | mtpxor 1687 |
[Holland] p.
1519 | Theorem 2 | sumdmdi 28663 |
[Holland] p.
1520 | Lemma 5 | cdj1i 28676 cdj3i 28684 cdj3lem1 28677 cdjreui 28675 |
[Holland] p.
1524 | Lemma 7 | mddmdin0i 28674 |
[Holland95]
p. 13 | Theorem 3.6 | hlathil 36271 |
[Holland95]
p. 14 | Line 15 | hgmapvs 36201 |
[Holland95]
p. 14 | Line 16 | hdmaplkr 36223 |
[Holland95]
p. 14 | Line 17 | hdmapellkr 36224 |
[Holland95]
p. 14 | Line 19 | hdmapglnm2 36221 |
[Holland95]
p. 14 | Line 20 | hdmapip0com 36227 |
[Holland95]
p. 14 | Theorem 3.6 | hdmapevec2 36146 |
[Holland95]
p. 14 | Lines 24 and 25 | hdmapoc 36241 |
[Holland95] p.
204 | Definition of involution | df-srng 18669 |
[Holland95]
p. 212 | Definition of subspace | df-psubsp 33807 |
[Holland95]
p. 214 | Lemma 3.3 | lclkrlem2v 35835 |
[Holland95]
p. 214 | Definition 3.2 | df-lpolN 35788 |
[Holland95]
p. 214 | Definition of nonsingular | pnonsingN 34237 |
[Holland95]
p. 215 | Lemma 3.3(1) | dihoml4 35684 poml4N 34257 |
[Holland95]
p. 215 | Lemma 3.3(2) | dochexmid 35775 pexmidALTN 34282 pexmidN 34273 |
[Holland95]
p. 218 | Theorem 3.6 | lclkr 35840 |
[Holland95]
p. 218 | Definition of dual vector space | df-ldual 33429 ldualset 33430 |
[Holland95]
p. 222 | Item 1 | df-lines 33805 df-pointsN 33806 |
[Holland95]
p. 222 | Item 2 | df-polarityN 34207 |
[Holland95]
p. 223 | Remark | ispsubcl2N 34251 omllaw4 33551 pol1N 34214 polcon3N 34221 |
[Holland95]
p. 223 | Definition | df-psubclN 34239 |
[Holland95]
p. 223 | Equation for polarity | polval2N 34210 |
[Hughes] p.
44 | Equation 1.21b | ax-his3 27325 |
[Hughes] p.
47 | Definition of projection operator | dfpjop 28425 |
[Hughes] p.
49 | Equation 1.30 | eighmre 28206 eigre 28078 eigrei 28077 |
[Hughes] p.
49 | Equation 1.31 | eighmorth 28207 eigorth 28081 eigorthi 28080 |
[Hughes] p.
137 | Remark (ii) | eigposi 28079 |
[Huneke] p. 1 | Claim
1 | frgrancvvdeq 26569 frgrancvvdgeq 26570 frgrncvvdeq 41480 |
[Huneke] p. 1 | Statement
1 | frgrancvvdeqlemA 26564 frgrncvvdeqlemA 41476 |
[Huneke] p. 1 | Statement
2 | frgrancvvdeqlemB 26565 frgrncvvdeqlemB 41477 |
[Huneke] p. 1 | Statement
3 | frgrancvvdeqlemC 26566 frgrncvvdeqlemC 41478 |
[Huneke] p. 2 | Claim
2 | frgraregorufr 26580 frgraregorufr0 26579 frgraregorufrg 26599 frgrregorufr 41490 frgrregorufr0 41489 frgrregorufrg 41505 |
[Huneke] p. 2 | Claim
3 | frghash2spot 26590 frgregordn0 26597 frgrhash2wsp 41497 frrusgraord 26598 frrusgrord 41504 frrusgrord0 41503 |
[Huneke] p. 2 | Statement
4 | frgrawopreglem4 26574 frgrwopreglem4 41484 |
[Huneke] p. 2 | Statement
5 | frgrawopreg1 26577 frgrawopreg2 26578 frgrwopreg1 41487 frgrwopreg2 41488 |
[Huneke] p. 2 | Statement
6 | frgrawopreglem5 26575 frgrwopreglem5 41485 |
[Huneke] p.
2 | Statement 7 | fusgreghash2wspv 41499 usgreghash2spotv 26593 |
[Huneke] p.
2 | Statement 8 | fusgreghash2wsp 41502 usgreghash2spot 26596 |
[Huneke] p.
2 | Statement 9 | av-numclwwlk1 41528 av-numclwwlk8 41546 clwlkndivn 26380 clwlksndivn 41279 numclwwlk1 26625 numclwwlk8 26642 |
[Huneke] p. 2 | Definition
3 | frgrawopreglem1 26571 frgrwopreglem1 41481 |
[Huneke] p. 2 | Definition
4 | df-clwlk 26278 df-clwlks 40977 |
[Huneke] p.
2 | Definition 5 | av-numclwwlkovf 41511 numclwwlkovf 26608 |
[Huneke] p.
2 | Definition 6 | av-numclwwlkovg 41518 numclwwlkovg 26614 |
[Huneke] p.
2 | Definition 7 | av-numclwwlkovh 41531 numclwwlkovh 26628 |
[Huneke] p.
2 | Statement 10 | av-numclwwlk2 41537 numclwwlk2 26634 |
[Huneke] p. 2 | Statement
11 | rusgranumwlk 26484 rusgranumwlkg 26485 rusgrnumwlkg 41180 |
[Huneke] p.
2 | Statement 12 | av-numclwwlk3 41539 numclwwlk3 26636 |
[Huneke] p.
2 | Statement 13 | av-numclwwlk5 41542 numclwwlk5 26639 |
[Huneke] p.
2 | Statement 14 | av-numclwwlk7 41545 numclwwlk7 26641 |
[Indrzejczak] p.
33 | Definition ` `E | natded 26652 natded 26652 |
[Indrzejczak] p.
33 | Definition ` `I | natded 26652 |
[Indrzejczak] p.
34 | Definition ` `E | natded 26652 natded 26652 |
[Indrzejczak] p.
34 | Definition ` `I | natded 26652 |
[Jech] p. 4 | Definition of
class | cv 1474 cvjust 2605 |
[Jech] p. 42 | Lemma
6.1 | alephexp1 9280 |
[Jech] p. 42 | Equation
6.1 | alephadd 9278 alephmul 9279 |
[Jech] p. 43 | Lemma
6.2 | infmap 9277 infmap2 8923 |
[Jech] p. 71 | Lemma
9.3 | jech9.3 8560 |
[Jech] p. 72 | Equation
9.3 | scott0 8632 scottex 8631 |
[Jech] p. 72 | Exercise
9.1 | rankval4 8613 |
[Jech] p. 72 | Scheme
"Collection Principle" | cp 8637 |
[Jech] p.
78 | Note | opthprc 5089 |
[JonesMatijasevic] p.
694 | Definition 2.3 | rmxyval 36498 |
[JonesMatijasevic] p. 695 | Lemma
2.15 | jm2.15nn0 36588 |
[JonesMatijasevic] p. 695 | Lemma
2.16 | jm2.16nn0 36589 |
[JonesMatijasevic] p.
695 | Equation 2.7 | rmxadd 36510 |
[JonesMatijasevic] p.
695 | Equation 2.8 | rmyadd 36514 |
[JonesMatijasevic] p.
695 | Equation 2.9 | rmxp1 36515 rmyp1 36516 |
[JonesMatijasevic] p.
695 | Equation 2.10 | rmxm1 36517 rmym1 36518 |
[JonesMatijasevic] p.
695 | Equation 2.11 | rmx0 36508 rmx1 36509 rmxluc 36519 |
[JonesMatijasevic] p.
695 | Equation 2.12 | rmy0 36512 rmy1 36513 rmyluc 36520 |
[JonesMatijasevic] p.
695 | Equation 2.13 | rmxdbl 36522 |
[JonesMatijasevic] p.
695 | Equation 2.14 | rmydbl 36523 |
[JonesMatijasevic] p. 696 | Lemma
2.17 | jm2.17a 36545 jm2.17b 36546 jm2.17c 36547 |
[JonesMatijasevic] p. 696 | Lemma
2.19 | jm2.19 36578 |
[JonesMatijasevic] p. 696 | Lemma
2.20 | jm2.20nn 36582 |
[JonesMatijasevic] p.
696 | Theorem 2.18 | jm2.18 36573 |
[JonesMatijasevic] p. 697 | Lemma
2.24 | jm2.24 36548 jm2.24nn 36544 |
[JonesMatijasevic] p. 697 | Lemma
2.26 | jm2.26 36587 |
[JonesMatijasevic] p. 697 | Lemma
2.27 | jm2.27 36593 rmygeid 36549 |
[JonesMatijasevic] p. 698 | Lemma
3.1 | jm3.1 36605 |
[Juillerat]
p. 11 | Section *5 | etransc 39176 etransclem47 39174 etransclem48 39175 |
[Juillerat]
p. 12 | Equation (7) | etransclem44 39171 |
[Juillerat]
p. 12 | Equation *(7) | etransclem46 39173 |
[Juillerat]
p. 12 | Proof of the derivative calculated | etransclem32 39159 |
[Juillerat]
p. 13 | Proof | etransclem35 39162 |
[Juillerat]
p. 13 | Part of case 2 proven in | etransclem38 39165 |
[Juillerat]
p. 13 | Part of case 2 proven | etransclem24 39151 |
[Juillerat]
p. 13 | Part of case 2: proven in | etransclem41 39168 |
[Juillerat]
p. 14 | Proof | etransclem23 39150 |
[KalishMontague] p.
81 | Note 1 | ax-6 1875 |
[KalishMontague] p.
85 | Lemma 2 | equid 1926 |
[KalishMontague] p.
85 | Lemma 3 | equcomi 1931 |
[KalishMontague] p.
86 | Lemma 7 | cbvalivw 1921 cbvaliw 1920 |
[KalishMontague] p.
87 | Lemma 8 | spimvw 1914 spimw 1913 |
[KalishMontague] p.
87 | Lemma 9 | spfw 1952 spw 1954 |
[Kalmbach]
p. 14 | Definition of lattice | chabs1 27759 chabs1i 27761 chabs2 27760 chabs2i 27762 chjass 27776 chjassi 27729 latabs1 16910 latabs2 16911 |
[Kalmbach]
p. 15 | Definition of atom | df-at 28581 ela 28582 |
[Kalmbach]
p. 15 | Definition of covers | cvbr2 28526 cvrval2 33579 |
[Kalmbach]
p. 16 | Definition | df-ol 33483 df-oml 33484 |
[Kalmbach]
p. 20 | Definition of commutes | cmbr 27827 cmbri 27833 cmtvalN 33516 df-cm 27826 df-cmtN 33482 |
[Kalmbach]
p. 22 | Remark | omllaw5N 33552 pjoml5 27856 pjoml5i 27831 |
[Kalmbach]
p. 22 | Definition | pjoml2 27854 pjoml2i 27828 |
[Kalmbach]
p. 22 | Theorem 2(v) | cmcm 27857 cmcmi 27835 cmcmii 27840 cmtcomN 33554 |
[Kalmbach]
p. 22 | Theorem 2(ii) | omllaw3 33550 omlsi 27647 pjoml 27679 pjomli 27678 |
[Kalmbach]
p. 22 | Definition of OML law | omllaw2N 33549 |
[Kalmbach]
p. 23 | Remark | cmbr2i 27839 cmcm3 27858 cmcm3i 27837 cmcm3ii 27842 cmcm4i 27838 cmt3N 33556 cmt4N 33557 cmtbr2N 33558 |
[Kalmbach]
p. 23 | Lemma 3 | cmbr3 27851 cmbr3i 27843 cmtbr3N 33559 |
[Kalmbach]
p. 25 | Theorem 5 | fh1 27861 fh1i 27864 fh2 27862 fh2i 27865 omlfh1N 33563 |
[Kalmbach]
p. 65 | Remark | chjatom 28600 chslej 27741 chsleji 27701 shslej 27623 shsleji 27613 |
[Kalmbach]
p. 65 | Proposition 1 | chocin 27738 chocini 27697 chsupcl 27583 chsupval2 27653 h0elch 27496 helch 27484 hsupval2 27652 ocin 27539 ococss 27536 shococss 27537 |
[Kalmbach]
p. 65 | Definition of subspace sum | shsval 27555 |
[Kalmbach]
p. 66 | Remark | df-pjh 27638 pjssmi 28408 pjssmii 27924 |
[Kalmbach]
p. 67 | Lemma 3 | osum 27888 osumi 27885 |
[Kalmbach]
p. 67 | Lemma 4 | pjci 28443 |
[Kalmbach]
p. 103 | Exercise 6 | atmd2 28643 |
[Kalmbach]
p. 103 | Exercise 12 | mdsl0 28553 |
[Kalmbach]
p. 140 | Remark | hatomic 28603 hatomici 28602 hatomistici 28605 |
[Kalmbach]
p. 140 | Proposition 1 | atlatmstc 33624 |
[Kalmbach]
p. 140 | Proposition 1(i) | atexch 28624 lsatexch 33348 |
[Kalmbach]
p. 140 | Proposition 1(ii) | chcv1 28598 cvlcvr1 33644 cvr1 33714 |
[Kalmbach]
p. 140 | Proposition 1(iii) | cvexch 28617 cvexchi 28612 cvrexch 33724 |
[Kalmbach]
p. 149 | Remark 2 | chrelati 28607 hlrelat 33706 hlrelat5N 33705 lrelat 33319 |
[Kalmbach] p.
153 | Exercise 5 | lsmcv 18962 lsmsatcv 33315 spansncv 27896 spansncvi 27895 |
[Kalmbach]
p. 153 | Proposition 1(ii) | lsmcv2 33334 spansncv2 28536 |
[Kalmbach]
p. 266 | Definition | df-st 28454 |
[Kalmbach2]
p. 8 | Definition of adjoint | df-adjh 28092 |
[KanamoriPincus] p.
415 | Theorem 1.1 | fpwwe 9347 fpwwe2 9344 |
[KanamoriPincus] p.
416 | Corollary 1.3 | canth4 9348 |
[KanamoriPincus] p.
417 | Corollary 1.6 | canthp1 9355 |
[KanamoriPincus] p.
417 | Corollary 1.4(a) | canthnum 9350 |
[KanamoriPincus] p.
417 | Corollary 1.4(b) | canthwe 9352 |
[KanamoriPincus] p.
418 | Proposition 1.7 | pwfseq 9365 |
[KanamoriPincus] p.
419 | Lemma 2.2 | gchcdaidm 9369 gchxpidm 9370 |
[KanamoriPincus] p.
419 | Theorem 2.1 | gchacg 9381 gchhar 9380 |
[KanamoriPincus] p.
420 | Lemma 2.3 | pwcdadom 8921 unxpwdom 8377 |
[KanamoriPincus] p.
421 | Proposition 3.1 | gchpwdom 9371 |
[Kreyszig] p.
3 | Property M1 | metcl 21947 xmetcl 21946 |
[Kreyszig] p.
4 | Property M2 | meteq0 21954 |
[Kreyszig] p.
8 | Definition 1.1-8 | dscmet 22187 |
[Kreyszig] p.
12 | Equation 5 | conjmul 10621 muleqadd 10550 |
[Kreyszig] p.
18 | Definition 1.3-2 | mopnval 22053 |
[Kreyszig] p.
19 | Remark | mopntopon 22054 |
[Kreyszig] p.
19 | Theorem T1 | mopn0 22113 mopnm 22059 |
[Kreyszig] p.
19 | Theorem T2 | unimopn 22111 |
[Kreyszig] p.
19 | Definition of neighborhood | neibl 22116 |
[Kreyszig] p.
20 | Definition 1.3-3 | metcnp2 22157 |
[Kreyszig] p.
25 | Definition 1.4-1 | lmbr 20872 lmmbr 22864 lmmbr2 22865 |
[Kreyszig] p. 26 | Lemma
1.4-2(a) | lmmo 20994 |
[Kreyszig] p.
28 | Theorem 1.4-5 | lmcau 22919 |
[Kreyszig] p.
28 | Definition 1.4-3 | iscau 22882 iscmet2 22900 |
[Kreyszig] p.
30 | Theorem 1.4-7 | cmetss 22921 |
[Kreyszig] p.
30 | Theorem 1.4-6(a) | 1stcelcls 21074 metelcls 22911 |
[Kreyszig] p.
30 | Theorem 1.4-6(b) | metcld 22912 metcld2 22913 |
[Kreyszig] p.
51 | Equation 2 | clmvneg1 22707 lmodvneg1 18729 nvinv 26878 vcm 26815 |
[Kreyszig] p.
51 | Equation 1a | clm0vs 22703 lmod0vs 18719 slmd0vs 29108 vc0 26813 |
[Kreyszig] p.
51 | Equation 1b | lmodvs0 18720 slmdvs0 29109 vcz 26814 |
[Kreyszig] p.
58 | Definition 2.2-1 | imsmet 26930 ngpmet 22217 nrmmetd 22189 |
[Kreyszig] p.
59 | Equation 1 | imsdval 26925 imsdval2 26926 ncvspds 22769 ngpds 22218 |
[Kreyszig] p.
63 | Problem 1 | nmval 22204 nvnd 26927 |
[Kreyszig] p.
64 | Problem 2 | nmeq0 22232 nmge0 22231 nvge0 26912 nvz 26908 |
[Kreyszig] p.
64 | Problem 3 | nmrtri 22238 nvabs 26911 |
[Kreyszig] p.
91 | Definition 2.7-1 | isblo3i 27040 |
[Kreyszig] p.
92 | Equation 2 | df-nmoo 26984 |
[Kreyszig] p.
97 | Theorem 2.7-9(a) | blocn 27046 blocni 27044 |
[Kreyszig] p.
97 | Theorem 2.7-9(b) | lnocni 27045 |
[Kreyszig] p.
129 | Definition 3.1-1 | cphipeq0 22812 ipeq0 19802 ipz 26958 |
[Kreyszig] p.
135 | Problem 2 | pythi 27089 |
[Kreyszig] p.
137 | Lemma 3-2.1(a) | sii 27093 |
[Kreyszig] p.
144 | Equation 4 | supcvg 14427 |
[Kreyszig] p.
144 | Theorem 3.3-1 | minvec 23015 minveco 27124 |
[Kreyszig] p.
196 | Definition 3.9-1 | df-aj 26989 |
[Kreyszig] p.
247 | Theorem 4.7-2 | bcth 22934 |
[Kreyszig] p.
249 | Theorem 4.7-3 | ubth 27113 |
[Kreyszig]
p. 470 | Definition of positive operator ordering | leop 28366 leopg 28365 |
[Kreyszig]
p. 476 | Theorem 9.4-2 | opsqrlem2 28384 |
[Kreyszig] p.
525 | Theorem 10.1-1 | htth 27159 |
[Kulpa] p.
547 | Theorem | poimir 32612 |
[Kulpa] p.
547 | Equation (1) | poimirlem32 32611 |
[Kulpa] p.
547 | Equation (2) | poimirlem31 32610 |
[Kulpa] p.
548 | Theorem | broucube 32613 |
[Kulpa] p.
548 | Equation (6) | poimirlem26 32605 |
[Kulpa] p.
548 | Equation (7) | poimirlem27 32606 |
[Kunen] p. 10 | Axiom
0 | ax6e 2238 axnul 4716 |
[Kunen] p. 11 | Axiom
3 | axnul 4716 |
[Kunen] p. 12 | Axiom
6 | zfrep6 7027 |
[Kunen] p. 24 | Definition
10.24 | mapval 7756 mapvalg 7754 |
[Kunen] p. 30 | Lemma
10.20 | fodom 9227 |
[Kunen] p. 31 | Definition
10.24 | mapex 7750 |
[Kunen] p. 95 | Definition
2.1 | df-r1 8510 |
[Kunen] p. 97 | Lemma
2.10 | r1elss 8552 r1elssi 8551 |
[Kunen] p. 107 | Exercise
4 | rankop 8604 rankopb 8598 rankuni 8609 rankxplim 8625 rankxpsuc 8628 |
[KuratowskiMostowski] p.
109 | Section. Eq. 14 | iuniin 4467 |
[Lang] p.
3 | Definition | df-mnd 17118 |
[Lang] p.
7 | Definition | dfgrp2e 17271 |
[Lang] p.
53 | Definition | df-cat 16152 |
[Lang] p.
54 | Definition | df-iso 16232 |
[Lang] p.
57 | Definition | df-inito 16464 df-termo 16465 |
[Lang] p.
58 | Example | irinitoringc 41861 |
[Lang] p.
58 | Statement | initoeu1 16484 termoeu1 16491 |
[Lang] p.
62 | Definition | df-func 16341 |
[Lang] p.
65 | Definition | df-nat 16426 |
[Lang] p.
91 | Note | df-ringc 41797 |
[Lang] p.
128 | Remark | dsmmlmod 19908 |
[Lang] p.
129 | Proof | lincscm 42013 lincscmcl 42015 lincsum 42012 lincsumcl 42014 |
[Lang] p.
129 | Statement | lincolss 42017 |
[Lang] p.
129 | Observation | dsmmfi 19901 |
[Lang] p.
147 | Definition | snlindsntor 42054 |
[Lang] p.
504 | Statement | mat1 20072 matring 20068 |
[Lang] p.
504 | Definition | df-mamu 20009 |
[Lang] p.
505 | Statement | mamuass 20027 mamutpos 20083 matassa 20069 mattposvs 20080 tposmap 20082 |
[Lang] p.
513 | Definition | mdet1 20226 mdetf 20220 |
[Lang] p. 513 | Theorem
4.4 | cramer 20316 |
[Lang] p. 514 | Proposition
4.6 | mdetleib 20212 |
[Lang] p. 514 | Proposition
4.8 | mdettpos 20236 |
[Lang] p.
515 | Definition | df-minmar1 20260 smadiadetr 20300 |
[Lang] p. 515 | Corollary
4.9 | mdetero 20235 mdetralt 20233 |
[Lang] p. 517 | Proposition
4.15 | mdetmul 20248 |
[Lang] p.
518 | Definition | df-madu 20259 |
[Lang] p. 518 | Proposition
4.16 | madulid 20270 madurid 20269 matinv 20302 |
[Lang] p. 561 | Theorem
3.1 | cayleyhamilton 20514 |
[Lang], p.
561 | Remark | chpmatply1 20456 |
[Lang], p.
561 | Definition | df-chpmat 20451 |
[LarsonHostetlerEdwards] p.
278 | Section 4.1 | dvconstbi 37555 |
[LarsonHostetlerEdwards] p.
311 | Example 1a | lhe4.4ex1a 37550 |
[LarsonHostetlerEdwards] p.
375 | Theorem 5.1 | expgrowth 37556 |
[LeBlanc] p. 277 | Rule
R2 | axnul 4716 |
[Levy] p.
338 | Axiom | df-clab 2597 df-clel 2606 df-cleq 2603 |
[Levy58] p. 2 | Definition
I | isfin1-3 9091 |
[Levy58] p. 2 | Definition
II | df-fin2 8991 |
[Levy58] p. 2 | Definition
Ia | df-fin1a 8990 |
[Levy58] p. 2 | Definition
III | df-fin3 8993 |
[Levy58] p. 3 | Definition
V | df-fin5 8994 |
[Levy58] p. 3 | Definition
IV | df-fin4 8992 |
[Levy58] p. 4 | Definition
VI | df-fin6 8995 |
[Levy58] p. 4 | Definition
VII | df-fin7 8996 |
[Levy58], p. 3 | Theorem
1 | fin1a2 9120 |
[Lopez-Astorga] p.
12 | Rule 1 | mptnan 1684 |
[Lopez-Astorga] p.
12 | Rule 2 | mptxor 1685 |
[Lopez-Astorga] p.
12 | Rule 3 | mtpxor 1687 |
[Maeda] p.
167 | Theorem 1(d) to (e) | mdsymlem6 28651 |
[Maeda] p.
168 | Lemma 5 | mdsym 28655 mdsymi 28654 |
[Maeda] p.
168 | Lemma 4(i) | mdsymlem4 28649 mdsymlem6 28651 mdsymlem7 28652 |
[Maeda] p.
168 | Lemma 4(ii) | mdsymlem8 28653 |
[MaedaMaeda] p. 1 | Remark | ssdmd1 28556 ssdmd2 28557 ssmd1 28554 ssmd2 28555 |
[MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 28552 |
[MaedaMaeda] p. 1 | Definition
1.1 | df-dmd 28524 df-md 28523 mdbr 28537 |
[MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 28574 mdslj1i 28562 mdslj2i 28563 mdslle1i 28560 mdslle2i 28561 mdslmd1i 28572 mdslmd2i 28573 |
[MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 28564 mdsl2bi 28566 mdsl2i 28565 |
[MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 28578 |
[MaedaMaeda] p. 2 | Lemma
1.5.1 | mdslmd3i 28575 |
[MaedaMaeda] p. 2 | Lemma
1.5.2 | mdslmd4i 28576 |
[MaedaMaeda] p. 2 | Lemma
1.5.3 | mdsl0 28553 |
[MaedaMaeda] p. 2 | Theorem
1.3 | dmdsl3 28558 mdsl3 28559 |
[MaedaMaeda] p. 3 | Theorem
1.9.1 | csmdsymi 28577 |
[MaedaMaeda] p. 4 | Theorem
1.14 | mdcompli 28672 |
[MaedaMaeda] p. 30 | Lemma
7.2 | atlrelat1 33626 hlrelat1 33704 |
[MaedaMaeda] p. 31 | Lemma
7.5 | lcvexch 33344 |
[MaedaMaeda] p. 31 | Lemma
7.5.1 | cvmd 28579 cvmdi 28567 cvnbtwn4 28532 cvrnbtwn4 33584 |
[MaedaMaeda] p. 31 | Lemma
7.5.2 | cvdmd 28580 |
[MaedaMaeda] p. 31 | Definition
7.4 | cvlcvrp 33645 cvp 28618 cvrp 33720 lcvp 33345 |
[MaedaMaeda] p. 31 | Theorem
7.6(b) | atmd 28642 |
[MaedaMaeda] p. 31 | Theorem
7.6(c) | atdmd 28641 |
[MaedaMaeda] p. 32 | Definition
7.8 | cvlexch4N 33638 hlexch4N 33696 |
[MaedaMaeda] p. 34 | Exercise
7.1 | atabsi 28644 |
[MaedaMaeda] p. 41 | Lemma
9.2(delta) | cvrat4 33747 |
[MaedaMaeda] p. 61 | Definition
15.1 | 0psubN 34053 atpsubN 34057 df-pointsN 33806 pointpsubN 34055 |
[MaedaMaeda] p. 62 | Theorem
15.5 | df-pmap 33808 pmap11 34066 pmaple 34065 pmapsub 34072 pmapval 34061 |
[MaedaMaeda] p. 62 | Theorem
15.5.1 | pmap0 34069 pmap1N 34071 |
[MaedaMaeda] p. 62 | Theorem
15.5.2 | pmapglb 34074 pmapglb2N 34075 pmapglb2xN 34076 pmapglbx 34073 |
[MaedaMaeda] p. 63 | Equation
15.5.3 | pmapjoin 34156 |
[MaedaMaeda] p. 67 | Postulate
PS1 | ps-1 33781 |
[MaedaMaeda] p. 68 | Lemma
16.2 | df-padd 34100 paddclN 34146 paddidm 34145 |
[MaedaMaeda] p. 68 | Condition
PS2 | ps-2 33782 |
[MaedaMaeda] p. 68 | Equation
16.2.1 | paddass 34142 |
[MaedaMaeda] p. 69 | Lemma
16.4 | ps-1 33781 |
[MaedaMaeda] p. 69 | Theorem
16.4 | ps-2 33782 |
[MaedaMaeda] p.
70 | Theorem 16.9 | lsmmod 17911 lsmmod2 17912 lssats 33317 shatomici 28601 shatomistici 28604 shmodi 27633 shmodsi 27632 |
[MaedaMaeda] p. 130 | Remark
29.6 | dmdmd 28543 mdsymlem7 28652 |
[MaedaMaeda] p. 132 | Theorem
29.13(e) | pjoml6i 27832 |
[MaedaMaeda] p. 136 | Lemma
31.1.5 | shjshseli 27736 |
[MaedaMaeda] p. 139 | Remark | sumdmdii 28658 |
[Margaris] p. 40 | Rule
C | exlimiv 1845 |
[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 385 df-ex 1696 df-or 384 dfbi2 658 |
[Margaris] p.
51 | Theorem 1 | idALT 23 |
[Margaris] p.
56 | Theorem 3 | conventions 26650 |
[Margaris]
p. 59 | Section 14 | notnotrALTVD 38173 |
[Margaris] p.
60 | Theorem 8 | mth8 157 |
[Margaris]
p. 60 | Section 14 | con3ALTVD 38174 |
[Margaris]
p. 79 | Rule C | exinst01 37871 exinst11 37872 |
[Margaris] p.
89 | Theorem 19.2 | 19.2 1879 19.2g 2046 r19.2z 4012 |
[Margaris] p.
89 | Theorem 19.3 | 19.3 2057 rr19.3v 3314 |
[Margaris] p.
89 | Theorem 19.5 | alcom 2024 |
[Margaris] p.
89 | Theorem 19.6 | alex 1743 |
[Margaris] p.
89 | Theorem 19.7 | alnex 1697 |
[Margaris] p.
89 | Theorem 19.8 | 19.8a 2039 |
[Margaris] p.
89 | Theorem 19.9 | 19.9 2060 19.9h 2106 exlimd 2074 exlimdh 2134 |
[Margaris] p.
89 | Theorem 19.11 | excom 2029 excomim 2030 |
[Margaris] p.
89 | Theorem 19.12 | 19.12 2150 |
[Margaris] p.
90 | Section 19 | conventions-label 26651 conventions-label 26651 conventions-label 26651 conventions-label 26651 |
[Margaris] p.
90 | Theorem 19.14 | exnal 1744 |
[Margaris]
p. 90 | Theorem 19.15 | 2albi 37599 albi 1736 |
[Margaris] p.
90 | Theorem 19.16 | 19.16 2080 |
[Margaris] p.
90 | Theorem 19.17 | 19.17 2081 |
[Margaris]
p. 90 | Theorem 19.18 | 2exbi 37601 exbi 1762 |
[Margaris] p.
90 | Theorem 19.19 | 19.19 2084 |
[Margaris]
p. 90 | Theorem 19.20 | 2alim 37598 2alimdv 1834 alimd 2068 alimdh 1735 alimdv 1832 ax-4 1728
ralimdaa 2941 ralimdv 2946 ralimdva 2945 ralimdvva 2947 sbcimdv 3465 |
[Margaris] p.
90 | Theorem 19.21 | 19.21 2062 19.21h 2107 19.21t 2061 19.21vv 37597 alrimd 2071 alrimdd 2070 alrimdh 1777 alrimdv 1844 alrimi 2069 alrimih 1741 alrimiv 1842 alrimivv 1843 hbralrimi 2937 r19.21be 2917 r19.21bi 2916 ralrimd 2942 ralrimdv 2951 ralrimdva 2952 ralrimdvv 2956 ralrimdvva 2957 ralrimi 2940 ralrimiv 2948 ralrimiva 2949 ralrimivv 2953 ralrimivva 2954 ralrimivvva 2955 ralrimivw 2950 |
[Margaris]
p. 90 | Theorem 19.22 | 2exim 37600 2eximdv 1835 exim 1751
eximd 2072 eximdh 1778 eximdv 1833 rexim 2991 reximd2a 2996 reximdai 2995 reximddv 3001 reximddv2 3002 reximdv 2999 reximdv2 2997 reximdva 3000 reximdvai 2998 reximi2 2993 |
[Margaris] p.
90 | Theorem 19.23 | 19.23 2067 19.23bi 2049 19.23h 2108 exlimdv 1848 exlimdvv 1849 exlimexi 37751 exlimiv 1845 exlimivv 1847 rexlimdv 3012 rexlimdv3a 3015 rexlimdva 3013 rexlimdvaa 3014 rexlimdvv 3019 rexlimdvva 3020 rexlimdvw 3016 rexlimiv 3009 rexlimiva 3010 rexlimivv 3018 |
[Margaris] p.
90 | Theorem 19.24 | 19.24 1887 |
[Margaris] p.
90 | Theorem 19.25 | 19.25 1797 |
[Margaris] p.
90 | Theorem 19.26 | 19.26 1786 |
[Margaris] p.
90 | Theorem 19.27 | 19.27 2082 r19.27z 4022 r19.27zv 4023 |
[Margaris] p.
90 | Theorem 19.28 | 19.28 2083 19.28vv 37607 r19.28z 4015 r19.28zv 4018 rr19.28v 3315 |
[Margaris] p.
90 | Theorem 19.29 | 19.29 1789 r19.29d2r 3061 r19.29imd 3056 |
[Margaris] p.
90 | Theorem 19.30 | 19.30 1798 |
[Margaris] p.
90 | Theorem 19.31 | 19.31 2089 19.31vv 37605 |
[Margaris] p.
90 | Theorem 19.32 | 19.32 2088 r19.32 39816 |
[Margaris]
p. 90 | Theorem 19.33 | 19.33-2 37603 19.33 1801 |
[Margaris] p.
90 | Theorem 19.34 | 19.34 1888 |
[Margaris] p.
90 | Theorem 19.35 | 19.35 1794 |
[Margaris] p.
90 | Theorem 19.36 | 19.36 2085 19.36vv 37604 r19.36zv 4024 |
[Margaris] p.
90 | Theorem 19.37 | 19.37 2087 19.37vv 37606 r19.37zv 4019 |
[Margaris] p.
90 | Theorem 19.38 | 19.38 1757 |
[Margaris] p.
90 | Theorem 19.39 | 19.39 1886 |
[Margaris] p.
90 | Theorem 19.40 | 19.40-2 1803 19.40 1785 r19.40 3069 |
[Margaris] p.
90 | Theorem 19.41 | 19.41 2090 19.41rg 37787 |
[Margaris] p.
90 | Theorem 19.42 | 19.42 2092 |
[Margaris] p.
90 | Theorem 19.43 | 19.43 1799 |
[Margaris] p.
90 | Theorem 19.44 | 19.44 2093 r19.44zv 4021 |
[Margaris] p.
90 | Theorem 19.45 | 19.45 2094 r19.45zv 4020 |
[Margaris] p.
90 | Theorem 1977.23 | 19.23t 2066 |
[Margaris] p.
110 | Exercise 2(b) | eu1 2498 |
[Mayet] p.
370 | Remark | jpi 28513 largei 28510 stri 28500 |
[Mayet3] p.
9 | Definition of CH-states | df-hst 28455 ishst 28457 |
[Mayet3] p.
10 | Theorem | hstrbi 28509 hstri 28508 |
[Mayet3] p.
1223 | Theorem 4.1 | mayete3i 27971 |
[Mayet3] p.
1240 | Theorem 7.1 | mayetes3i 27972 |
[MegPav2000] p. 2344 | Theorem
3.3 | stcltrthi 28521 |
[MegPav2000] p. 2345 | Definition
3.4-1 | chintcl 27575 chsupcl 27583 |
[MegPav2000] p. 2345 | Definition
3.4-2 | hatomic 28603 |
[MegPav2000] p. 2345 | Definition
3.4-3(a) | superpos 28597 |
[MegPav2000] p. 2345 | Definition
3.4-3(b) | atexch 28624 |
[MegPav2000] p. 2366 | Figure
7 | pl42N 34287 |
[MegPav2002] p.
362 | Lemma 2.2 | latj31 16922 latj32 16920 latjass 16918 |
[Megill] p. 444 | Axiom
C5 | ax-5 1827 ax5ALT 33210 |
[Megill] p. 444 | Section
7 | conventions 26650 |
[Megill] p.
445 | Lemma L12 | aecom-o 33204 ax-c11n 33191 axc11n 2295 |
[Megill] p. 446 | Lemma
L17 | equtrr 1936 |
[Megill] p.
446 | Lemma L18 | ax6fromc10 33199 |
[Megill] p.
446 | Lemma L19 | hbnae-o 33231 hbnae 2305 |
[Megill] p. 447 | Remark
9.1 | df-sb 1868 sbid 2100
sbidd-misc 42259 sbidd 42258 |
[Megill] p. 448 | Remark
9.6 | axc14 2360 |
[Megill] p.
448 | Scheme C4' | ax-c4 33187 |
[Megill] p.
448 | Scheme C5' | ax-c5 33186 sp 2041 |
[Megill] p. 448 | Scheme
C6' | ax-11 2021 |
[Megill] p.
448 | Scheme C7' | ax-c7 33188 |
[Megill] p. 448 | Scheme
C8' | ax-7 1922 |
[Megill] p.
448 | Scheme C9' | ax-c9 33193 |
[Megill] p. 448 | Scheme
C10' | ax-6 1875 ax-c10 33189 |
[Megill] p.
448 | Scheme C11' | ax-c11 33190 |
[Megill] p. 448 | Scheme
C12' | ax-8 1979 |
[Megill] p. 448 | Scheme
C13' | ax-9 1986 |
[Megill] p.
448 | Scheme C14' | ax-c14 33194 |
[Megill] p.
448 | Scheme C15' | ax-c15 33192 |
[Megill] p.
448 | Scheme C16' | ax-c16 33195 |
[Megill] p.
448 | Theorem 9.4 | dral1-o 33207 dral1 2313 dral2-o 33233 dral2 2312 drex1 2315 drex2 2316 drsb1 2365 drsb2 2366 |
[Megill] p. 449 | Theorem
9.7 | sbcom2 2433 sbequ 2364 sbid2v 2445 |
[Megill] p.
450 | Example in Appendix | hba1-o 33200 hba1 2137 |
[Mendelson]
p. 35 | Axiom A3 | hirstL-ax3 39708 |
[Mendelson] p.
36 | Lemma 1.8 | idALT 23 |
[Mendelson] p.
69 | Axiom 4 | rspsbc 3484 rspsbca 3485 stdpc4 2341 |
[Mendelson]
p. 69 | Axiom 5 | ax-c4 33187 ra4 3491
stdpc5 2063 |
[Mendelson] p.
81 | Rule C | exlimiv 1845 |
[Mendelson] p.
95 | Axiom 6 | stdpc6 1944 |
[Mendelson] p.
95 | Axiom 7 | stdpc7 1945 |
[Mendelson] p.
225 | Axiom system NBG | ru 3401 |
[Mendelson] p.
230 | Exercise 4.8(b) | opthwiener 4901 |
[Mendelson] p.
231 | Exercise 4.10(k) | inv1 3922 |
[Mendelson] p.
231 | Exercise 4.10(l) | unv 3923 |
[Mendelson] p.
231 | Exercise 4.10(n) | dfin3 3825 |
[Mendelson] p.
231 | Exercise 4.10(o) | df-nul 3875 |
[Mendelson] p.
231 | Exercise 4.10(q) | dfin4 3826 |
[Mendelson] p.
231 | Exercise 4.10(s) | ddif 3704 |
[Mendelson] p.
231 | Definition of union | dfun3 3824 |
[Mendelson] p.
235 | Exercise 4.12(c) | univ 4846 |
[Mendelson] p.
235 | Exercise 4.12(d) | pwv 4371 |
[Mendelson] p.
235 | Exercise 4.12(j) | pwin 4942 |
[Mendelson] p.
235 | Exercise 4.12(k) | pwunss 4943 |
[Mendelson] p.
235 | Exercise 4.12(l) | pwssun 4944 |
[Mendelson] p.
235 | Exercise 4.12(n) | uniin 4393 |
[Mendelson] p.
235 | Exercise 4.12(p) | reli 5171 |
[Mendelson] p.
235 | Exercise 4.12(t) | relssdmrn 5573 |
[Mendelson] p.
244 | Proposition 4.8(g) | epweon 6875 |
[Mendelson] p.
246 | Definition of successor | df-suc 5646 |
[Mendelson] p.
250 | Exercise 4.36 | oelim2 7562 |
[Mendelson] p.
254 | Proposition 4.22(b) | xpen 8008 |
[Mendelson] p.
254 | Proposition 4.22(c) | xpsnen 7929 xpsneng 7930 |
[Mendelson] p.
254 | Proposition 4.22(d) | xpcomen 7936 xpcomeng 7937 |
[Mendelson] p.
254 | Proposition 4.22(e) | xpassen 7939 |
[Mendelson] p.
255 | Definition | brsdom 7864 |
[Mendelson] p.
255 | Exercise 4.39 | endisj 7932 |
[Mendelson] p.
255 | Exercise 4.41 | mapprc 7748 |
[Mendelson] p.
255 | Exercise 4.43 | mapsnen 7920 |
[Mendelson] p.
255 | Exercise 4.45 | mapunen 8014 |
[Mendelson] p.
255 | Exercise 4.47 | xpmapen 8013 |
[Mendelson] p.
255 | Exercise 4.42(a) | map0e 7781 |
[Mendelson] p.
255 | Exercise 4.42(b) | map1 7921 |
[Mendelson] p.
257 | Proposition 4.24(a) | undom 7933 |
[Mendelson] p.
258 | Exercise 4.56(b) | cdaen 8878 |
[Mendelson] p.
258 | Exercise 4.56(c) | cdaassen 8887 cdacomen 8886 |
[Mendelson] p.
258 | Exercise 4.56(f) | cdadom1 8891 |
[Mendelson] p.
258 | Exercise 4.56(g) | xp2cda 8885 |
[Mendelson] p.
258 | Definition of cardinal sum | cdaval 8875 df-cda 8873 |
[Mendelson] p.
266 | Proposition 4.34(a) | oa1suc 7498 |
[Mendelson] p.
266 | Proposition 4.34(f) | oaordex 7525 |
[Mendelson] p.
275 | Proposition 4.42(d) | entri3 9260 |
[Mendelson] p.
281 | Definition | df-r1 8510 |
[Mendelson] p.
281 | Proposition 4.45 (b) to (a) | unir1 8559 |
[Mendelson] p.
287 | Axiom system MK | ru 3401 |
[MertziosUnger] p.
152 | Definition | df-frgr 41429 |
[MertziosUnger] p.
153 | Remark 1 | frconngra 26548 frgrconngr 41464 |
[MertziosUnger] p.
153 | Remark 2 | vdgn1frgrav2 26553 vdgn1frgrav3 26555 vdgn1frgrv2 41466 vdgn1frgrv3 41467 vdn1frgrav2 26552 |
[MertziosUnger] p.
153 | Remark 3 | vdgfrgragt2 26554 vdgfrgrgt2 41468 |
[MertziosUnger] p. 153 | Proposition
1(a) | n4cyclfrgr 41461 n4cyclfrgra 26545 |
[MertziosUnger] p. 153 | Proposition
1(b) | 2pthfrgr 41454 2pthfrgra 26538 2pthfrgrarn 26536 2pthfrgrarn2 26537 2pthfrgrrn 41452 2pthfrgrrn2 41453 |
[Mittelstaedt] p.
9 | Definition | df-oc 27493 |
[Monk1] p.
22 | Remark | conventions 26650 |
[Monk1] p. 22 | Theorem
3.1 | conventions 26650 |
[Monk1] p. 26 | Theorem
2.8(vii) | ssin 3797 |
[Monk1] p. 33 | Theorem
3.2(i) | ssrel 5130 ssrelf 28805 |
[Monk1] p. 33 | Theorem
3.2(ii) | eqrel 5132 |
[Monk1] p. 34 | Definition
3.3 | df-opab 4644 |
[Monk1] p. 36 | Theorem
3.7(i) | coi1 5568 coi2 5569 |
[Monk1] p. 36 | Theorem
3.8(v) | dm0 5260 rn0 5298 |
[Monk1] p. 36 | Theorem
3.7(ii) | cnvi 5456 |
[Monk1] p. 37 | Theorem
3.13(i) | relxp 5150 |
[Monk1] p. 37 | Theorem
3.13(x) | dmxp 5265 rnxp 5483 |
[Monk1] p. 37 | Theorem
3.13(ii) | 0xp 5122 xp0 5471 |
[Monk1] p. 38 | Theorem
3.16(ii) | ima0 5400 |
[Monk1] p. 38 | Theorem
3.16(viii) | imai 5397 |
[Monk1] p. 39 | Theorem
3.17 | imaex 6996 imaexg 6995 |
[Monk1] p. 39 | Theorem
3.16(xi) | imassrn 5396 |
[Monk1] p. 41 | Theorem
4.3(i) | fnopfv 6259 funfvop 6237 |
[Monk1] p. 42 | Theorem
4.3(ii) | funopfvb 6149 |
[Monk1] p. 42 | Theorem
4.4(iii) | fvelima 6158 |
[Monk1] p. 43 | Theorem
4.6 | funun 5846 |
[Monk1] p. 43 | Theorem
4.8(iv) | dff13 6416 dff13f 6417 |
[Monk1] p. 46 | Theorem
4.15(v) | funex 6387 funrnex 7026 |
[Monk1] p. 50 | Definition
5.4 | fniunfv 6409 |
[Monk1] p. 52 | Theorem
5.12(ii) | op2ndb 5537 |
[Monk1] p. 52 | Theorem
5.11(viii) | ssint 4428 |
[Monk1] p. 52 | Definition
5.13 (i) | 1stval2 7076 df-1st 7059 |
[Monk1] p. 52 | Definition
5.13 (ii) | 2ndval2 7077 df-2nd 7060 |
[Monk1] p. 112 | Theorem
15.17(v) | ranksn 8600 ranksnb 8573 |
[Monk1] p. 112 | Theorem
15.17(iv) | rankuni2 8601 |
[Monk1] p. 112 | Theorem
15.17(iii) | rankun 8602 rankunb 8596 |
[Monk1] p. 113 | Theorem
15.18 | r1val3 8584 |
[Monk1] p. 113 | Definition
15.19 | df-r1 8510 r1val2 8583 |
[Monk1] p.
117 | Lemma | zorn2 9211 zorn2g 9208 |
[Monk1] p. 133 | Theorem
18.11 | cardom 8695 |
[Monk1] p. 133 | Theorem
18.12 | canth3 9262 |
[Monk1] p. 133 | Theorem
18.14 | carduni 8690 |
[Monk2] p. 105 | Axiom
C4 | ax-4 1728 |
[Monk2] p. 105 | Axiom
C7 | ax-7 1922 |
[Monk2] p. 105 | Axiom
C8 | ax-12 2034 ax-c15 33192 ax12v2 2036 |
[Monk2] p.
108 | Lemma 5 | ax-c4 33187 |
[Monk2] p. 109 | Lemma
12 | ax-11 2021 |
[Monk2] p. 109 | Lemma
15 | equvini 2334 equvinv 1946 eqvinop 4881 |
[Monk2] p. 113 | Axiom
C5-1 | ax-5 1827 ax5ALT 33210 |
[Monk2] p. 113 | Axiom
C5-2 | ax-10 2006 |
[Monk2] p. 113 | Axiom
C5-3 | ax-11 2021 |
[Monk2] p. 114 | Lemma
21 | sp 2041 |
[Monk2] p. 114 | Lemma
22 | axc4 2115 hba1-o 33200 hba1 2137 |
[Monk2] p. 114 | Lemma
23 | nfia1 2017 |
[Monk2] p. 114 | Lemma
24 | nfa2 2027 nfra2 2930 |
[Moore] p. 53 | Part
I | df-mre 16069 |
[Munkres] p. 77 | Example
2 | distop 20610 indistop 20616 indistopon 20615 |
[Munkres] p. 77 | Example
3 | fctop 20618 fctop2 20619 |
[Munkres] p. 77 | Example
4 | cctop 20620 |
[Munkres] p.
78 | Definition of basis | df-bases 20522 isbasis3g 20564 |
[Munkres] p.
78 | Definition of a topology generated by a basis | df-topgen 15927 tgval2 20571 |
[Munkres] p.
79 | Remark | tgcl 20584 |
[Munkres] p. 80 | Lemma
2.1 | tgval3 20578 |
[Munkres] p. 80 | Lemma
2.2 | tgss2 20602 tgss3 20601 |
[Munkres] p. 81 | Lemma
2.3 | basgen 20603 basgen2 20604 |
[Munkres] p.
83 | Exercise 3 | topdifinf 32373 topdifinfeq 32374 topdifinffin 32372 topdifinfindis 32370 |
[Munkres] p.
89 | Definition of subspace topology | resttop 20774 |
[Munkres] p. 93 | Theorem
6.1(1) | 0cld 20652 topcld 20649 |
[Munkres] p. 93 | Theorem
6.1(2) | iincld 20653 |
[Munkres] p. 93 | Theorem
6.1(3) | uncld 20655 |
[Munkres] p.
94 | Definition of closure | clsval 20651 |
[Munkres] p.
94 | Definition of interior | ntrval 20650 |
[Munkres] p. 95 | Theorem
6.5(a) | clsndisj 20689 elcls 20687 |
[Munkres] p. 95 | Theorem
6.5(b) | elcls3 20697 |
[Munkres] p. 97 | Theorem
6.6 | clslp 20762 neindisj 20731 |
[Munkres] p.
97 | Corollary 6.7 | cldlp 20764 |
[Munkres] p.
97 | Definition of limit point | islp2 20759 lpval 20753 |
[Munkres] p.
98 | Definition of Hausdorff space | df-haus 20929 |
[Munkres] p.
102 | Definition of continuous function | df-cn 20841 iscn 20849 iscn2 20852 |
[Munkres] p.
107 | Theorem 7.2(g) | cncnp 20894 cncnp2 20895 cncnpi 20892 df-cnp 20842 iscnp 20851 iscnp2 20853 |
[Munkres] p.
127 | Theorem 10.1 | metcn 22158 |
[Munkres] p.
128 | Theorem 10.3 | metcn4 22917 |
[NielsenChuang] p. 195 | Equation
4.73 | unierri 28347 |
[OeSilva] p.
| Result | ax-bgbltosilva 40226 |
[Pfenning] p.
17 | Definition XM | natded 26652 |
[Pfenning] p.
17 | Definition NNC | natded 26652 notnotrd 127 |
[Pfenning] p.
17 | Definition ` `C | natded 26652 |
[Pfenning] p.
18 | Rule" | natded 26652 |
[Pfenning] p.
18 | Definition /\I | natded 26652 |
[Pfenning] p.
18 | Definition ` `E | natded 26652 natded 26652 natded 26652 natded 26652 natded 26652 |
[Pfenning] p.
18 | Definition ` `I | natded 26652 natded 26652 natded 26652 natded 26652 natded 26652 |
[Pfenning] p.
18 | Definition ` `EL | natded 26652 |
[Pfenning] p.
18 | Definition ` `ER | natded 26652 |
[Pfenning] p.
18 | Definition ` `Ea,u | natded 26652 |
[Pfenning] p.
18 | Definition ` `IR | natded 26652 |
[Pfenning] p.
18 | Definition ` `Ia | natded 26652 |
[Pfenning] p.
127 | Definition =E | natded 26652 |
[Pfenning] p.
127 | Definition =I | natded 26652 |
[Ponnusamy] p.
361 | Theorem 6.44 | cphip0l 22810 df-dip 26940 dip0l 26957 ip0l 19800 |
[Ponnusamy] p.
361 | Equation 6.45 | cphipval 22850 ipval 26942 |
[Ponnusamy] p.
362 | Equation I1 | dipcj 26953 ipcj 19798 |
[Ponnusamy] p.
362 | Equation I3 | cphdir 22813 dipdir 27081 ipdir 19803 ipdiri 27069 |
[Ponnusamy] p.
362 | Equation I4 | ipidsq 26949 nmsq 22802 |
[Ponnusamy] p.
362 | Equation 6.46 | ip0i 27064 |
[Ponnusamy] p.
362 | Equation 6.47 | ip1i 27066 |
[Ponnusamy] p.
362 | Equation 6.48 | ip2i 27067 |
[Ponnusamy] p.
363 | Equation I2 | cphass 22819 dipass 27084 ipass 19809 ipassi 27080 |
[Prugovecki] p. 186 | Definition of
bra | braval 28187 df-bra 28093 |
[Prugovecki] p. 376 | Equation
8.1 | df-kb 28094 kbval 28197 |
[PtakPulmannova] p. 66 | Proposition
3.2.17 | atomli 28625 |
[PtakPulmannova] p. 68 | Lemma
3.1.4 | df-pclN 34192 |
[PtakPulmannova] p. 68 | Lemma
3.2.20 | atcvat3i 28639 atcvat4i 28640 cvrat3 33746 cvrat4 33747 lsatcvat3 33357 |
[PtakPulmannova] p. 68 | Definition
3.2.18 | cvbr 28525 cvrval 33574 df-cv 28522 df-lcv 33324 lspsncv0 18967 |
[PtakPulmannova] p. 72 | Lemma
3.3.6 | pclfinN 34204 |
[PtakPulmannova] p. 74 | Lemma
3.3.10 | pclcmpatN 34205 |
[Quine] p. 16 | Definition
2.1 | df-clab 2597 rabid 3095 |
[Quine] p. 17 | Definition
2.1'' | dfsb7 2443 |
[Quine] p. 18 | Definition
2.7 | df-cleq 2603 |
[Quine] p. 19 | Definition
2.9 | conventions 26650 df-v 3175 |
[Quine] p. 34 | Theorem
5.1 | abeq2 2719 |
[Quine] p. 35 | Theorem
5.2 | abid1 2731 abid2f 2777 |
[Quine] p. 40 | Theorem
6.1 | sb5 2418 |
[Quine] p. 40 | Theorem
6.2 | sb56 2136 sb6 2417 |
[Quine] p. 41 | Theorem
6.3 | df-clel 2606 |
[Quine] p. 41 | Theorem
6.4 | eqid 2610 eqid1 26715 |
[Quine] p. 41 | Theorem
6.5 | eqcom 2617 |
[Quine] p. 42 | Theorem
6.6 | df-sbc 3403 |
[Quine] p. 42 | Theorem
6.7 | dfsbcq 3404 dfsbcq2 3405 |
[Quine] p. 43 | Theorem
6.8 | vex 3176 |
[Quine] p. 43 | Theorem
6.9 | isset 3180 |
[Quine] p. 44 | Theorem
7.3 | spcgf 3261 spcgv 3266 spcimgf 3259 |
[Quine] p. 44 | Theorem
6.11 | spsbc 3415 spsbcd 3416 |
[Quine] p. 44 | Theorem
6.12 | elex 3185 |
[Quine] p. 44 | Theorem
6.13 | elab 3319 elabg 3320 elabgf 3317 |
[Quine] p. 44 | Theorem
6.14 | noel 3878 |
[Quine] p. 48 | Theorem
7.2 | snprc 4197 |
[Quine] p. 48 | Definition
7.1 | df-pr 4128 df-sn 4126 |
[Quine] p. 49 | Theorem
7.4 | snss 4259 snssg 4268 |
[Quine] p. 49 | Theorem
7.5 | prss 4291 prssg 4290 |
[Quine] p. 49 | Theorem
7.6 | prid1 4241 prid1g 4239 prid2 4242 prid2g 4240 snid 4155
snidg 4153 |
[Quine] p. 51 | Theorem
7.12 | snex 4835 |
[Quine] p. 51 | Theorem
7.13 | prex 4836 |
[Quine] p. 53 | Theorem
8.2 | unisn 4387 unisnALT 38184 unisng 4388 |
[Quine] p. 53 | Theorem
8.3 | uniun 4392 |
[Quine] p. 54 | Theorem
8.6 | elssuni 4403 |
[Quine] p. 54 | Theorem
8.7 | uni0 4401 |
[Quine] p. 56 | Theorem
8.17 | uniabio 5778 |
[Quine] p. 56 | Definition
8.18 | dfiota2 5769 |
[Quine] p. 57 | Theorem
8.19 | iotaval 5779 |
[Quine] p. 57 | Theorem
8.22 | iotanul 5783 |
[Quine] p. 58 | Theorem
8.23 | iotaex 5785 |
[Quine] p. 58 | Definition
9.1 | df-op 4132 |
[Quine] p. 61 | Theorem
9.5 | opabid 4907 opelopab 4922 opelopaba 4916 opelopabaf 4924 opelopabf 4925 opelopabg 4918 opelopabga 4913 opelopabgf 4920 oprabid 6576 |
[Quine] p. 64 | Definition
9.11 | df-xp 5044 |
[Quine] p. 64 | Definition
9.12 | df-cnv 5046 |
[Quine] p. 64 | Definition
9.15 | df-id 4953 |
[Quine] p. 65 | Theorem
10.3 | fun0 5868 |
[Quine] p. 65 | Theorem
10.4 | funi 5834 |
[Quine] p. 65 | Theorem
10.5 | funsn 5853 funsng 5851 |
[Quine] p. 65 | Definition
10.1 | df-fun 5806 |
[Quine] p. 65 | Definition
10.2 | args 5412 dffv4 6100 |
[Quine] p. 68 | Definition
10.11 | conventions 26650 df-fv 5812 fv2 6098 |
[Quine] p. 124 | Theorem
17.3 | nn0opth2 12921 nn0opth2i 12920 nn0opthi 12919 omopthi 7624 |
[Quine] p. 177 | Definition
25.2 | df-rdg 7393 |
[Quine] p. 232 | Equation
i | carddom 9255 |
[Quine] p. 284 | Axiom
39(vi) | funimaex 5890 funimaexg 5889 |
[Quine] p. 331 | Axiom
system NF | ru 3401 |
[ReedSimon]
p. 36 | Definition (iii) | ax-his3 27325 |
[ReedSimon] p.
63 | Exercise 4(a) | df-dip 26940 polid 27400 polid2i 27398 polidi 27399 |
[ReedSimon] p.
63 | Exercise 4(b) | df-ph 27052 |
[ReedSimon]
p. 195 | Remark | lnophm 28262 lnophmi 28261 |
[Retherford] p. 49 | Exercise
1(i) | leopadd 28375 |
[Retherford] p. 49 | Exercise
1(ii) | leopmul 28377 leopmuli 28376 |
[Retherford] p. 49 | Exercise
1(iv) | leoptr 28380 |
[Retherford] p. 49 | Definition
VI.1 | df-leop 28095 leoppos 28369 |
[Retherford] p. 49 | Exercise
1(iii) | leoptri 28379 |
[Retherford] p. 49 | Definition of
operator ordering | leop3 28368 |
[Roman] p.
4 | Definition | df-dmat 20115 df-dmatalt 41981 |
[Roman] p.
18 | Part Preliminaries | df-rng0 41665 |
[Roman] p. 19 | Part
Preliminaries | df-ring 18372 |
[Roman] p.
46 | Theorem 1.6 | isldepslvec2 42068 |
[Roman] p.
112 | Note | isldepslvec2 42068 ldepsnlinc 42091 zlmodzxznm 42080 |
[Roman] p.
112 | Example | zlmodzxzequa 42079 zlmodzxzequap 42082 zlmodzxzldep 42087 |
[Roman] p. 170 | Theorem
7.8 | cayleyhamilton 20514 |
[Rosenlicht] p. 80 | Theorem | heicant 32614 |
[Rosser] p.
281 | Definition | df-op 4132 |
[Rotman] p.
28 | Remark | pgrpgt2nabl 41941 pmtr3ncom 17718 |
[Rotman] p. 31 | Theorem
3.4 | symggen2 17714 |
[Rotman] p. 42 | Theorem
3.15 | cayley 17657 cayleyth 17658 |
[Rudin] p. 164 | Equation
27 | efcan 14665 |
[Rudin] p. 164 | Equation
30 | efzval 14671 |
[Rudin] p. 167 | Equation
48 | absefi 14765 |
[Sanford] p.
39 | Remark | ax-mp 5 mto 187 |
[Sanford] p. 39 | Rule
3 | mtpxor 1687 |
[Sanford] p. 39 | Rule
4 | mptxor 1685 |
[Sanford] p. 40 | Rule
1 | mptnan 1684 |
[Schechter] p.
51 | Definition of antisymmetry | intasym 5430 |
[Schechter] p.
51 | Definition of irreflexivity | intirr 5433 |
[Schechter] p.
51 | Definition of symmetry | cnvsym 5429 |
[Schechter] p.
51 | Definition of transitivity | cotr 5427 |
[Schechter] p.
78 | Definition of Moore collection of sets | df-mre 16069 |
[Schechter] p.
79 | Definition of Moore closure | df-mrc 16070 |
[Schechter] p.
82 | Section 4.5 | df-mrc 16070 |
[Schechter] p.
84 | Definition (A) of an algebraic closure system | df-acs 16072 |
[Schechter] p.
139 | Definition AC3 | dfac9 8841 |
[Schechter]
p. 141 | Definition (MC) | dfac11 36650 |
[Schechter] p.
149 | Axiom DC1 | ax-dc 9151 axdc3 9159 |
[Schechter] p.
187 | Definition of ring with unit | isring 18374 isrngo 32866 |
[Schechter]
p. 276 | Remark 11.6.e | span0 27785 |
[Schechter]
p. 276 | Definition of span | df-span 27552 spanval 27576 |
[Schechter] p.
428 | Definition 15.35 | bastop1 20608 |
[Schwabhauser] p.
10 | Axiom A1 | axcgrrflx 25594 axtgcgrrflx 25161 |
[Schwabhauser] p.
10 | Axiom A2 | axcgrtr 25595 |
[Schwabhauser] p.
10 | Axiom A3 | axcgrid 25596 axtgcgrid 25162 |
[Schwabhauser] p.
10 | Axioms A1 to A3 | df-trkgc 25147 |
[Schwabhauser] p.
11 | Axiom A4 | axsegcon 25607 axtgsegcon 25163 df-trkgcb 25149 |
[Schwabhauser] p.
11 | Axiom A5 | ax5seg 25618 axtg5seg 25164 df-trkgcb 25149 |
[Schwabhauser] p.
11 | Axiom A6 | axbtwnid 25619 axtgbtwnid 25165 df-trkgb 25148 |
[Schwabhauser] p.
12 | Axiom A7 | axpasch 25621 axtgpasch 25166 df-trkgb 25148 |
[Schwabhauser] p.
12 | Axiom A8 | axlowdim2 25640 df-trkg2d 29996 |
[Schwabhauser] p.
13 | Axiom A8 | axtglowdim2 25169 |
[Schwabhauser] p.
13 | Axiom A9 | axtgupdim2 25170 df-trkg2d 29996 |
[Schwabhauser] p.
13 | Axiom A10 | axeuclid 25643 axtgeucl 25171 df-trkge 25150 |
[Schwabhauser] p.
13 | Axiom A11 | axcont 25656 axtgcont 25168 axtgcont1 25167 df-trkgb 25148 |
[Schwabhauser] p. 27 | Theorem
2.1 | cgrrflx 31264 |
[Schwabhauser] p. 27 | Theorem
2.2 | cgrcomim 31266 |
[Schwabhauser] p. 27 | Theorem
2.3 | cgrtr 31269 |
[Schwabhauser] p. 27 | Theorem
2.4 | cgrcoml 31273 |
[Schwabhauser] p. 27 | Theorem
2.5 | cgrcomr 31274 tgcgrcomimp 25172 tgcgrcoml 25174 tgcgrcomr 25173 |
[Schwabhauser] p. 28 | Theorem
2.8 | cgrtriv 31279 tgcgrtriv 25179 |
[Schwabhauser] p. 28 | Theorem
2.10 | 5segofs 31283 tg5segofs 30004 |
[Schwabhauser] p. 28 | Definition
2.10 | df-afs 30001 df-ofs 31260 |
[Schwabhauser] p. 29 | Theorem
2.11 | cgrextend 31285 tgcgrextend 25180 |
[Schwabhauser] p. 29 | Theorem
2.12 | segconeq 31287 tgsegconeq 25181 |
[Schwabhauser] p. 30 | Theorem
3.1 | btwnouttr2 31299 btwntriv2 31289 tgbtwntriv2 25182 |
[Schwabhauser] p. 30 | Theorem
3.2 | btwncomim 31290 tgbtwncom 25183 |
[Schwabhauser] p. 30 | Theorem
3.3 | btwntriv1 31293 tgbtwntriv1 25186 |
[Schwabhauser] p. 30 | Theorem
3.4 | btwnswapid 31294 tgbtwnswapid 25187 |
[Schwabhauser] p. 30 | Theorem
3.5 | btwnexch2 31300 btwnintr 31296 tgbtwnexch2 25191 tgbtwnintr 25188 |
[Schwabhauser] p. 30 | Theorem
3.6 | btwnexch 31302 btwnexch3 31297 tgbtwnexch 25193 tgbtwnexch3 25189 |
[Schwabhauser] p. 30 | Theorem
3.7 | btwnouttr 31301 tgbtwnouttr 25192 tgbtwnouttr2 25190 |
[Schwabhauser] p.
32 | Theorem 3.13 | axlowdim1 25639 |
[Schwabhauser] p. 32 | Theorem
3.14 | btwndiff 31304 tgbtwndiff 25201 |
[Schwabhauser] p.
33 | Theorem 3.17 | tgtrisegint 25194 trisegint 31305 |
[Schwabhauser] p. 34 | Theorem
4.2 | ifscgr 31321 tgifscgr 25203 |
[Schwabhauser] p.
34 | Theorem 4.11 | colcom 25253 colrot1 25254 colrot2 25255 lncom 25317 lnrot1 25318 lnrot2 25319 |
[Schwabhauser] p. 34 | Definition
4.1 | df-ifs 31317 |
[Schwabhauser] p. 35 | Theorem
4.3 | cgrsub 31322 tgcgrsub 25204 |
[Schwabhauser] p. 35 | Theorem
4.5 | cgrxfr 31332 tgcgrxfr 25213 |
[Schwabhauser] p.
35 | Statement 4.4 | ercgrg 25212 |
[Schwabhauser] p. 35 | Definition
4.4 | df-cgr3 31318 df-cgrg 25206 |
[Schwabhauser] p. 36 | Theorem
4.6 | btwnxfr 31333 tgbtwnxfr 25225 |
[Schwabhauser] p. 36 | Theorem
4.11 | colinearperm1 31339 colinearperm2 31341 colinearperm3 31340 colinearperm4 31342 colinearperm5 31343 |
[Schwabhauser] p.
36 | Definition 4.8 | df-ismt 25228 |
[Schwabhauser] p. 36 | Definition
4.10 | df-colinear 31316 tgellng 25248 tglng 25241 |
[Schwabhauser] p. 37 | Theorem
4.12 | colineartriv1 31344 |
[Schwabhauser] p. 37 | Theorem
4.13 | colinearxfr 31352 lnxfr 25261 |
[Schwabhauser] p. 37 | Theorem
4.14 | lineext 31353 lnext 25262 |
[Schwabhauser] p. 37 | Theorem
4.16 | fscgr 31357 tgfscgr 25263 |
[Schwabhauser] p. 37 | Theorem
4.17 | linecgr 31358 lncgr 25264 |
[Schwabhauser] p. 37 | Definition
4.15 | df-fs 31319 |
[Schwabhauser] p. 38 | Theorem
4.18 | lineid 31360 lnid 25265 |
[Schwabhauser] p. 38 | Theorem
4.19 | idinside 31361 tgidinside 25266 |
[Schwabhauser] p. 39 | Theorem
5.1 | btwnconn1 31378 tgbtwnconn1 25270 |
[Schwabhauser] p. 41 | Theorem
5.2 | btwnconn2 31379 tgbtwnconn2 25271 |
[Schwabhauser] p. 41 | Theorem
5.3 | btwnconn3 31380 tgbtwnconn3 25272 |
[Schwabhauser] p. 41 | Theorem
5.5 | brsegle2 31386 |
[Schwabhauser] p. 41 | Definition
5.4 | df-segle 31384 legov 25280 |
[Schwabhauser] p.
41 | Definition 5.5 | legov2 25281 |
[Schwabhauser] p.
42 | Remark 5.13 | legso 25294 |
[Schwabhauser] p. 42 | Theorem
5.6 | seglecgr12im 31387 |
[Schwabhauser] p. 42 | Theorem
5.7 | seglerflx 31389 |
[Schwabhauser] p. 42 | Theorem
5.8 | segletr 31391 |
[Schwabhauser] p. 42 | Theorem
5.9 | segleantisym 31392 |
[Schwabhauser] p. 42 | Theorem
5.10 | seglelin 31393 |
[Schwabhauser] p. 42 | Theorem
5.11 | seglemin 31390 |
[Schwabhauser] p. 42 | Theorem
5.12 | colinbtwnle 31395 |
[Schwabhauser] p.
42 | Proposition 5.7 | legid 25282 |
[Schwabhauser] p.
42 | Proposition 5.8 | legtrd 25284 |
[Schwabhauser] p.
42 | Proposition 5.9 | legtri3 25285 |
[Schwabhauser] p.
42 | Proposition 5.10 | legtrid 25286 |
[Schwabhauser] p.
42 | Proposition 5.11 | leg0 25287 |
[Schwabhauser] p. 43 | Theorem
6.2 | btwnoutside 31402 |
[Schwabhauser] p. 43 | Theorem
6.3 | broutsideof3 31403 |
[Schwabhauser] p. 43 | Theorem
6.4 | broutsideof 31398 df-outsideof 31397 |
[Schwabhauser] p. 43 | Definition
6.1 | broutsideof2 31399 ishlg 25297 |
[Schwabhauser] p.
44 | Theorem 6.4 | hlln 25302 |
[Schwabhauser] p.
44 | Theorem 6.5 | hlid 25304 outsideofrflx 31404 |
[Schwabhauser] p.
44 | Theorem 6.6 | hlcomb 25298 hlcomd 25299 outsideofcom 31405 |
[Schwabhauser] p.
44 | Theorem 6.7 | hltr 25305 outsideoftr 31406 |
[Schwabhauser] p.
44 | Theorem 6.11 | hlcgreu 25313 outsideofeu 31408 |
[Schwabhauser] p. 44 | Definition
6.8 | df-ray 31415 |
[Schwabhauser] p. 45 | Part
2 | df-lines2 31416 |
[Schwabhauser] p. 45 | Theorem
6.13 | outsidele 31409 |
[Schwabhauser] p. 45 | Theorem
6.15 | lineunray 31424 |
[Schwabhauser] p. 45 | Theorem
6.16 | lineelsb2 31425 tglineelsb2 25327 |
[Schwabhauser] p. 45 | Theorem
6.17 | linecom 31427 linerflx1 31426 linerflx2 31428 tglinecom 25330 tglinerflx1 25328 tglinerflx2 25329 |
[Schwabhauser] p. 45 | Theorem
6.18 | linethru 31430 tglinethru 25331 |
[Schwabhauser] p. 45 | Definition
6.14 | df-line2 31414 tglng 25241 |
[Schwabhauser] p.
45 | Proposition 6.13 | legbtwn 25289 |
[Schwabhauser] p. 46 | Theorem
6.19 | linethrueu 31433 tglinethrueu 25334 |
[Schwabhauser] p. 46 | Theorem
6.21 | lineintmo 31434 tglineineq 25338 tglineinteq 25340 tglineintmo 25337 |
[Schwabhauser] p.
46 | Theorem 6.23 | colline 25344 |
[Schwabhauser] p.
46 | Theorem 6.24 | tglowdim2l 25345 |
[Schwabhauser] p.
46 | Theorem 6.25 | tglowdim2ln 25346 |
[Schwabhauser] p.
49 | Theorem 7.3 | mirinv 25361 |
[Schwabhauser] p.
49 | Theorem 7.7 | mirmir 25357 |
[Schwabhauser] p.
49 | Theorem 7.8 | mirreu3 25349 |
[Schwabhauser] p.
49 | Definition 7.5 | df-mir 25348 ismir 25354 mirbtwn 25353 mircgr 25352 mirfv 25351 mirval 25350 |
[Schwabhauser] p.
50 | Theorem 7.8 | mirreu 25359 |
[Schwabhauser] p.
50 | Theorem 7.9 | mireq 25360 |
[Schwabhauser] p.
50 | Theorem 7.10 | mirinv 25361 |
[Schwabhauser] p.
50 | Theorem 7.11 | mirf1o 25364 |
[Schwabhauser] p.
50 | Theorem 7.13 | miriso 25365 |
[Schwabhauser] p.
51 | Theorem 7.14 | mirmot 25370 |
[Schwabhauser] p.
51 | Theorem 7.15 | mirbtwnb 25367 mirbtwni 25366 |
[Schwabhauser] p.
51 | Theorem 7.16 | mircgrs 25368 |
[Schwabhauser] p.
51 | Theorem 7.17 | miduniq 25380 |
[Schwabhauser] p.
52 | Lemma 7.21 | symquadlem 25384 |
[Schwabhauser] p.
52 | Theorem 7.18 | miduniq1 25381 |
[Schwabhauser] p.
52 | Theorem 7.19 | miduniq2 25382 |
[Schwabhauser] p.
52 | Theorem 7.20 | colmid 25383 |
[Schwabhauser] p.
53 | Lemma 7.22 | krippen 25386 |
[Schwabhauser] p.
55 | Lemma 7.25 | midexlem 25387 |
[Schwabhauser] p.
57 | Theorem 8.2 | ragcom 25393 |
[Schwabhauser] p.
57 | Definition 8.1 | df-rag 25389 israg 25392 |
[Schwabhauser] p.
58 | Theorem 8.3 | ragcol 25394 |
[Schwabhauser] p.
58 | Theorem 8.4 | ragmir 25395 |
[Schwabhauser] p.
58 | Theorem 8.5 | ragtrivb 25397 |
[Schwabhauser] p.
58 | Theorem 8.6 | ragflat2 25398 |
[Schwabhauser] p.
58 | Theorem 8.7 | ragflat 25399 |
[Schwabhauser] p.
58 | Theorem 8.8 | ragtriva 25400 |
[Schwabhauser] p.
58 | Theorem 8.9 | ragflat3 25401 ragncol 25404 |
[Schwabhauser] p.
58 | Theorem 8.10 | ragcgr 25402 |
[Schwabhauser] p.
59 | Theorem 8.12 | perpcom 25408 |
[Schwabhauser] p.
59 | Theorem 8.13 | ragperp 25412 |
[Schwabhauser] p.
59 | Theorem 8.14 | perpneq 25409 |
[Schwabhauser] p.
59 | Definition 8.11 | df-perpg 25391 isperp 25407 |
[Schwabhauser] p.
59 | Definition 8.13 | isperp2 25410 |
[Schwabhauser] p.
60 | Theorem 8.18 | foot 25414 |
[Schwabhauser] p.
62 | Lemma 8.20 | colperpexlem1 25422 colperpexlem2 25423 |
[Schwabhauser] p.
63 | Theorem 8.21 | colperpex 25425 colperpexlem3 25424 |
[Schwabhauser] p.
64 | Theorem 8.22 | mideu 25430 midex 25429 |
[Schwabhauser] p.
66 | Lemma 8.24 | opphllem 25427 |
[Schwabhauser] p.
67 | Theorem 9.2 | oppcom 25436 |
[Schwabhauser] p.
67 | Definition 9.1 | islnopp 25431 |
[Schwabhauser] p.
68 | Lemma 9.3 | opphllem2 25440 |
[Schwabhauser] p.
68 | Lemma 9.4 | opphllem5 25443 opphllem6 25444 |
[Schwabhauser] p.
69 | Theorem 9.5 | opphl 25446 |
[Schwabhauser] p.
69 | Theorem 9.6 | axtgpasch 25166 |
[Schwabhauser] p.
70 | Theorem 9.6 | outpasch 25447 |
[Schwabhauser] p.
71 | Theorem 9.8 | lnopp2hpgb 25455 |
[Schwabhauser] p.
71 | Definition 9.7 | df-hpg 25450 hpgbr 25452 |
[Schwabhauser] p.
72 | Lemma 9.10 | hpgerlem 25457 |
[Schwabhauser] p.
72 | Theorem 9.9 | lnoppnhpg 25456 |
[Schwabhauser] p.
72 | Theorem 9.11 | hpgid 25458 |
[Schwabhauser] p.
72 | Theorem 9.12 | hpgcom 25459 |
[Schwabhauser] p.
72 | Theorem 9.13 | hpgtr 25460 |
[Schwabhauser] p.
73 | Theorem 9.18 | colopp 25461 |
[Schwabhauser] p.
73 | Theorem 9.19 | colhp 25462 |
[Schwabhauser] p.
88 | Theorem 10.2 | lmieu 25476 |
[Schwabhauser] p.
88 | Definition 10.1 | df-mid 25466 |
[Schwabhauser] p.
89 | Theorem 10.4 | lmicom 25480 |
[Schwabhauser] p.
89 | Theorem 10.5 | lmilmi 25481 |
[Schwabhauser] p.
89 | Theorem 10.6 | lmireu 25482 |
[Schwabhauser] p.
89 | Theorem 10.7 | lmieq 25483 |
[Schwabhauser] p.
89 | Theorem 10.8 | lmiinv 25484 |
[Schwabhauser] p.
89 | Theorem 10.9 | lmif1o 25487 |
[Schwabhauser] p.
89 | Theorem 10.10 | lmiiso 25489 |
[Schwabhauser] p.
89 | Definition 10.3 | df-lmi 25467 |
[Schwabhauser] p.
90 | Theorem 10.11 | lmimot 25490 |
[Schwabhauser] p.
91 | Theorem 10.12 | hypcgr 25493 |
[Schwabhauser] p.
92 | Theorem 10.14 | lmiopp 25494 |
[Schwabhauser] p.
92 | Theorem 10.15 | lnperpex 25495 |
[Schwabhauser] p.
92 | Theorem 10.16 | trgcopy 25496 trgcopyeu 25498 |
[Schwabhauser] p.
95 | Definition 11.2 | dfcgra2 25521 |
[Schwabhauser] p.
95 | Definition 11.3 | iscgra 25501 |
[Schwabhauser] p.
95 | Proposition 11.4 | cgracgr 25510 |
[Schwabhauser] p.
95 | Proposition 11.10 | cgrahl1 25508 cgrahl2 25509 |
[Schwabhauser] p.
96 | Theorem 11.6 | cgraid 25511 |
[Schwabhauser] p.
96 | Theorem 11.9 | cgraswap 25512 |
[Schwabhauser] p.
97 | Theorem 11.7 | cgracom 25514 |
[Schwabhauser] p.
97 | Theorem 11.8 | cgratr 25515 |
[Schwabhauser] p.
97 | Theorem 11.21 | cgrabtwn 25517 cgrahl 25518 |
[Schwabhauser] p.
98 | Theorem 11.13 | sacgr 25522 |
[Schwabhauser] p.
98 | Theorem 11.14 | oacgr 25523 |
[Schwabhauser] p.
98 | Theorem 11.15 | acopy 25524 acopyeu 25525 |
[Schwabhauser] p.
101 | Theorem 11.24 | inagswap 25530 |
[Schwabhauser] p.
101 | Theorem 11.25 | inaghl 25531 |
[Schwabhauser] p.
101 | Property for point ` ` to lie in the angle ` ` Defnition
11.23 | isinag 25529 |
[Schwabhauser] p.
102 | Lemma 11.28 | cgrg3col4 25534 |
[Schwabhauser] p.
102 | Definition 11.27 | df-leag 25532 isleag 25533 |
[Schwabhauser] p.
107 | Theorem 11.49 | tgsas 25536 tgsas1 25535 tgsas2 25537 tgsas3 25538 |
[Schwabhauser] p.
108 | Theorem 11.50 | tgasa 25540 tgasa1 25539 |
[Schwabhauser] p.
109 | Theorem 11.51 | tgsss1 25541 tgsss2 25542 tgsss3 25543 |
[Shapiro] p.
230 | Theorem 6.5.1 | dchrhash 24796 dchrsum 24794 dchrsum2 24793 sumdchr 24797 |
[Shapiro] p.
232 | Theorem 6.5.2 | dchr2sum 24798 sum2dchr 24799 |
[Shapiro], p. 199 | Lemma
6.1C.2 | ablfacrp 18288 ablfacrp2 18289 |
[Shapiro], p.
328 | Equation 9.2.4 | vmasum 24741 |
[Shapiro], p.
329 | Equation 9.2.7 | logfac2 24742 |
[Shapiro], p.
329 | Equation 9.2.9 | logfacrlim 24749 |
[Shapiro], p.
331 | Equation 9.2.13 | vmadivsum 24971 |
[Shapiro], p.
331 | Equation 9.2.14 | rplogsumlem2 24974 |
[Shapiro], p.
336 | Exercise 9.1.7 | vmalogdivsum 25028 vmalogdivsum2 25027 |
[Shapiro], p.
375 | Theorem 9.4.1 | dirith 25018 dirith2 25017 |
[Shapiro], p.
375 | Equation 9.4.3 | rplogsum 25016 rpvmasum 25015 rpvmasum2 25001 |
[Shapiro], p.
376 | Equation 9.4.7 | rpvmasumlem 24976 |
[Shapiro], p.
376 | Equation 9.4.8 | dchrvmasum 25014 |
[Shapiro], p. 377 | Lemma
9.4.1 | dchrisum 24981 dchrisumlem1 24978 dchrisumlem2 24979 dchrisumlem3 24980 dchrisumlema 24977 |
[Shapiro], p.
377 | Equation 9.4.11 | dchrvmasumlem1 24984 |
[Shapiro], p.
379 | Equation 9.4.16 | dchrmusum 25013 dchrmusumlem 25011 dchrvmasumlem 25012 |
[Shapiro], p. 380 | Lemma
9.4.2 | dchrmusum2 24983 |
[Shapiro], p. 380 | Lemma
9.4.3 | dchrvmasum2lem 24985 |
[Shapiro], p. 382 | Lemma
9.4.4 | dchrisum0 25009 dchrisum0re 25002 dchrisumn0 25010 |
[Shapiro], p.
382 | Equation 9.4.27 | dchrisum0fmul 24995 |
[Shapiro], p.
382 | Equation 9.4.29 | dchrisum0flb 24999 |
[Shapiro], p.
383 | Equation 9.4.30 | dchrisum0fno1 25000 |
[Shapiro], p.
403 | Equation 10.1.16 | pntrsumbnd 25055 pntrsumbnd2 25056 pntrsumo1 25054 |
[Shapiro], p.
405 | Equation 10.2.1 | mudivsum 25019 |
[Shapiro], p.
406 | Equation 10.2.6 | mulogsum 25021 |
[Shapiro], p.
407 | Equation 10.2.7 | mulog2sumlem1 25023 |
[Shapiro], p.
407 | Equation 10.2.8 | mulog2sum 25026 |
[Shapiro], p.
418 | Equation 10.4.6 | logsqvma 25031 |
[Shapiro], p.
418 | Equation 10.4.8 | logsqvma2 25032 |
[Shapiro], p.
419 | Equation 10.4.10 | selberg 25037 |
[Shapiro], p.
420 | Equation 10.4.12 | selberg2lem 25039 |
[Shapiro], p.
420 | Equation 10.4.14 | selberg2 25040 |
[Shapiro], p.
422 | Equation 10.6.7 | selberg3 25048 |
[Shapiro], p.
422 | Equation 10.4.20 | selberg4lem1 25049 |
[Shapiro], p.
422 | Equation 10.4.21 | selberg3lem1 25046 selberg3lem2 25047 |
[Shapiro], p.
422 | Equation 10.4.23 | selberg4 25050 |
[Shapiro], p.
427 | Theorem 10.5.2 | chpdifbnd 25044 |
[Shapiro], p.
428 | Equation 10.6.2 | selbergr 25057 |
[Shapiro], p.
429 | Equation 10.6.8 | selberg3r 25058 |
[Shapiro], p.
430 | Equation 10.6.11 | selberg4r 25059 |
[Shapiro], p.
431 | Equation 10.6.15 | pntrlog2bnd 25073 |
[Shapiro], p.
434 | Equation 10.6.27 | pntlema 25085 pntlemb 25086 pntlemc 25084 pntlemd 25083 pntlemg 25087 |
[Shapiro], p.
435 | Equation 10.6.29 | pntlema 25085 |
[Shapiro], p. 436 | Lemma
10.6.1 | pntpbnd 25077 |
[Shapiro], p. 436 | Lemma
10.6.2 | pntibnd 25082 |
[Shapiro], p.
436 | Equation 10.6.34 | pntlema 25085 |
[Shapiro], p.
436 | Equation 10.6.35 | pntlem3 25098 pntleml 25100 |
[Stoll] p. 13 | Definition
corresponds to | dfsymdif3 3852 |
[Stoll] p. 16 | Exercise
4.4 | 0dif 3929 dif0 3904 |
[Stoll] p. 16 | Exercise
4.8 | difdifdir 4008 |
[Stoll] p. 17 | Theorem
5.1(5) | unvdif 3994 |
[Stoll] p. 19 | Theorem
5.2(13) | undm 3844 |
[Stoll] p. 19 | Theorem
5.2(13') | indm 3845 |
[Stoll] p.
20 | Remark | invdif 3827 |
[Stoll] p. 25 | Definition
of ordered triple | df-ot 4134 |
[Stoll] p.
43 | Definition | uniiun 4509 |
[Stoll] p.
44 | Definition | intiin 4510 |
[Stoll] p.
45 | Definition | df-iin 4458 |
[Stoll] p. 45 | Definition
indexed union | df-iun 4457 |
[Stoll] p. 176 | Theorem
3.4(27) | iman 439 |
[Stoll] p. 262 | Example
4.1 | dfsymdif3 3852 |
[Strang] p.
242 | Section 6.3 | expgrowth 37556 |
[Suppes] p. 22 | Theorem
2 | eq0 3888 eq0f 3884 |
[Suppes] p. 22 | Theorem
4 | eqss 3583 eqssd 3585 eqssi 3584 |
[Suppes] p. 23 | Theorem
5 | ss0 3926 ss0b 3925 |
[Suppes] p. 23 | Theorem
6 | sstr 3576 sstrALT2 38092 |
[Suppes] p. 23 | Theorem
7 | pssirr 3669 |
[Suppes] p. 23 | Theorem
8 | pssn2lp 3670 |
[Suppes] p. 23 | Theorem
9 | psstr 3673 |
[Suppes] p. 23 | Theorem
10 | pssss 3664 |
[Suppes] p. 25 | Theorem
12 | elin 3758 elun 3715 |
[Suppes] p. 26 | Theorem
15 | inidm 3784 |
[Suppes] p. 26 | Theorem
16 | in0 3920 |
[Suppes] p. 27 | Theorem
23 | unidm 3718 |
[Suppes] p. 27 | Theorem
24 | un0 3919 |
[Suppes] p. 27 | Theorem
25 | ssun1 3738 |
[Suppes] p. 27 | Theorem
26 | ssequn1 3745 |
[Suppes] p. 27 | Theorem
27 | unss 3749 |
[Suppes] p. 27 | Theorem
28 | indir 3834 |
[Suppes] p. 27 | Theorem
29 | undir 3835 |
[Suppes] p. 28 | Theorem
32 | difid 3902 |
[Suppes] p. 29 | Theorem
33 | difin 3823 |
[Suppes] p. 29 | Theorem
34 | indif 3828 |
[Suppes] p. 29 | Theorem
35 | undif1 3995 |
[Suppes] p. 29 | Theorem
36 | difun2 4000 |
[Suppes] p. 29 | Theorem
37 | difin0 3993 |
[Suppes] p. 29 | Theorem
38 | disjdif 3992 |
[Suppes] p. 29 | Theorem
39 | difundi 3838 |
[Suppes] p. 29 | Theorem
40 | difindi 3840 |
[Suppes] p. 30 | Theorem
41 | nalset 4723 |
[Suppes] p. 39 | Theorem
61 | uniss 4394 |
[Suppes] p. 39 | Theorem
65 | uniop 4902 |
[Suppes] p. 41 | Theorem
70 | intsn 4448 |
[Suppes] p. 42 | Theorem
71 | intpr 4445 intprg 4446 |
[Suppes] p. 42 | Theorem
73 | op1stb 4867 |
[Suppes] p. 42 | Theorem
78 | intun 4444 |
[Suppes] p.
44 | Definition 15(a) | dfiun2 4490 dfiun2g 4488 |
[Suppes] p.
44 | Definition 15(b) | dfiin2 4491 |
[Suppes] p. 47 | Theorem
86 | elpw 4114 elpw2 4755 elpw2g 4754 elpwg 4116 elpwgdedVD 38175 |
[Suppes] p. 47 | Theorem
87 | pwid 4122 |
[Suppes] p. 47 | Theorem
89 | pw0 4283 |
[Suppes] p. 48 | Theorem
90 | pwpw0 4284 |
[Suppes] p. 52 | Theorem
101 | xpss12 5148 |
[Suppes] p. 52 | Theorem
102 | xpindi 5177 xpindir 5178 |
[Suppes] p. 52 | Theorem
103 | xpundi 5094 xpundir 5095 |
[Suppes] p. 54 | Theorem
105 | elirrv 8387 |
[Suppes] p. 58 | Theorem
2 | relss 5129 |
[Suppes] p. 59 | Theorem
4 | eldm 5243 eldm2 5244 eldm2g 5242 eldmg 5241 |
[Suppes] p.
59 | Definition 3 | df-dm 5048 |
[Suppes] p. 60 | Theorem
6 | dmin 5254 |
[Suppes] p. 60 | Theorem
8 | rnun 5460 |
[Suppes] p. 60 | Theorem
9 | rnin 5461 |
[Suppes] p.
60 | Definition 4 | dfrn2 5233 |
[Suppes] p. 61 | Theorem
11 | brcnv 5227 brcnvg 5225 |
[Suppes] p. 62 | Equation
5 | elcnv 5221 elcnv2 5222 |
[Suppes] p. 62 | Theorem
12 | relcnv 5422 |
[Suppes] p. 62 | Theorem
15 | cnvin 5459 |
[Suppes] p. 62 | Theorem
16 | cnvun 5457 |
[Suppes] p. 63 | Theorem
20 | co02 5566 |
[Suppes] p. 63 | Theorem
21 | dmcoss 5306 |
[Suppes] p.
63 | Definition 7 | df-co 5047 |
[Suppes] p. 64 | Theorem
26 | cnvco 5230 |
[Suppes] p. 64 | Theorem
27 | coass 5571 |
[Suppes] p. 65 | Theorem
31 | resundi 5330 |
[Suppes] p. 65 | Theorem
34 | elima 5390 elima2 5391 elima3 5392 elimag 5389 |
[Suppes] p. 65 | Theorem
35 | imaundi 5464 |
[Suppes] p. 66 | Theorem
40 | dminss 5466 |
[Suppes] p. 66 | Theorem
41 | imainss 5467 |
[Suppes] p. 67 | Exercise
11 | cnvxp 5470 |
[Suppes] p.
81 | Definition 34 | dfec2 7632 |
[Suppes] p. 82 | Theorem
72 | elec 7673 elecg 7672 |
[Suppes] p. 82 | Theorem
73 | erth 7678 erth2 7679 |
[Suppes] p. 83 | Theorem
74 | erdisj 7681 |
[Suppes] p. 89 | Theorem
96 | map0b 7782 |
[Suppes] p. 89 | Theorem
97 | map0 7784 map0g 7783 |
[Suppes] p. 89 | Theorem
98 | mapsn 7785 |
[Suppes] p. 89 | Theorem
99 | mapss 7786 |
[Suppes] p.
91 | Definition 12(ii) | alephsuc 8774 |
[Suppes] p.
91 | Definition 12(iii) | alephlim 8773 |
[Suppes] p. 92 | Theorem
1 | enref 7874 enrefg 7873 |
[Suppes] p. 92 | Theorem
2 | ensym 7891 ensymb 7890 ensymi 7892 |
[Suppes] p. 92 | Theorem
3 | entr 7894 |
[Suppes] p. 92 | Theorem
4 | unen 7925 |
[Suppes] p. 94 | Theorem
15 | endom 7868 |
[Suppes] p. 94 | Theorem
16 | ssdomg 7887 |
[Suppes] p. 94 | Theorem
17 | domtr 7895 |
[Suppes] p. 95 | Theorem
18 | sbth 7965 |
[Suppes] p. 97 | Theorem
23 | canth2 7998 canth2g 7999 |
[Suppes] p.
97 | Definition 3 | brsdom2 7969 df-sdom 7844 dfsdom2 7968 |
[Suppes] p. 97 | Theorem
21(i) | sdomirr 7982 |
[Suppes] p. 97 | Theorem
22(i) | domnsym 7971 |
[Suppes] p. 97 | Theorem
21(ii) | sdomnsym 7970 |
[Suppes] p. 97 | Theorem
22(ii) | domsdomtr 7980 |
[Suppes] p. 97 | Theorem
22(iv) | brdom2 7871 |
[Suppes] p. 97 | Theorem
21(iii) | sdomtr 7983 |
[Suppes] p. 97 | Theorem
22(iii) | sdomdomtr 7978 |
[Suppes] p. 98 | Exercise
4 | fundmen 7916 fundmeng 7917 |
[Suppes] p. 98 | Exercise
6 | xpdom3 7943 |
[Suppes] p. 98 | Exercise
11 | sdomentr 7979 |
[Suppes] p. 104 | Theorem
37 | fofi 8135 |
[Suppes] p. 104 | Theorem
38 | pwfi 8144 |
[Suppes] p. 105 | Theorem
40 | pwfi 8144 |
[Suppes] p. 111 | Axiom
for cardinal numbers | carden 9252 |
[Suppes] p.
130 | Definition 3 | df-tr 4681 |
[Suppes] p. 132 | Theorem
9 | ssonuni 6878 |
[Suppes] p.
134 | Definition 6 | df-suc 5646 |
[Suppes] p. 136 | Theorem
Schema 22 | findes 6988 finds 6984 finds1 6987 finds2 6986 |
[Suppes] p. 151 | Theorem
42 | isfinite 8432 isfinite2 8103 isfiniteg 8105 unbnn 8101 |
[Suppes] p.
162 | Definition 5 | df-ltnq 9619 df-ltpq 9611 |
[Suppes] p. 197 | Theorem
Schema 4 | tfindes 6954 tfinds 6951 tfinds2 6955 |
[Suppes] p. 209 | Theorem
18 | oaord1 7518 |
[Suppes] p. 209 | Theorem
21 | oaword2 7520 |
[Suppes] p. 211 | Theorem
25 | oaass 7528 |
[Suppes] p.
225 | Definition 8 | iscard2 8685 |
[Suppes] p. 227 | Theorem
56 | ondomon 9264 |
[Suppes] p. 228 | Theorem
59 | harcard 8687 |
[Suppes] p.
228 | Definition 12(i) | aleph0 8772 |
[Suppes] p. 228 | Theorem
Schema 61 | onintss 5692 |
[Suppes] p. 228 | Theorem
Schema 62 | onminesb 6890 onminsb 6891 |
[Suppes] p. 229 | Theorem
64 | alephval2 9273 |
[Suppes] p. 229 | Theorem
65 | alephcard 8776 |
[Suppes] p. 229 | Theorem
66 | alephord2i 8783 |
[Suppes] p. 229 | Theorem
67 | alephnbtwn 8777 |
[Suppes] p.
229 | Definition 12 | df-aleph 8649 |
[Suppes] p. 242 | Theorem
6 | weth 9200 |
[Suppes] p. 242 | Theorem
8 | entric 9258 |
[Suppes] p. 242 | Theorem
9 | carden 9252 |
[TakeutiZaring] p.
8 | Axiom 1 | ax-ext 2590 |
[TakeutiZaring] p.
13 | Definition 4.5 | df-cleq 2603 |
[TakeutiZaring] p.
13 | Proposition 4.6 | df-clel 2606 |
[TakeutiZaring] p.
13 | Proposition 4.9 | cvjust 2605 |
[TakeutiZaring] p.
13 | Proposition 4.7(3) | eqtr 2629 |
[TakeutiZaring] p.
14 | Definition 4.16 | df-oprab 6553 |
[TakeutiZaring] p.
14 | Proposition 4.14 | ru 3401 |
[TakeutiZaring] p.
15 | Axiom 2 | zfpair 4831 |
[TakeutiZaring] p.
15 | Exercise 1 | elpr 4146 elpr2 4147 elprg 4144 |
[TakeutiZaring] p.
15 | Exercise 2 | elsn 4140 elsn2 4158 elsn2g 4157 elsng 4139 velsn 4141 |
[TakeutiZaring] p.
15 | Exercise 3 | elop 4862 |
[TakeutiZaring] p.
15 | Exercise 4 | sneq 4135 sneqr 4311 |
[TakeutiZaring] p.
15 | Definition 5.1 | dfpr2 4143 dfsn2 4138 |
[TakeutiZaring] p.
16 | Axiom 3 | uniex 6851 |
[TakeutiZaring] p.
16 | Exercise 6 | opth 4871 |
[TakeutiZaring] p.
16 | Exercise 7 | opex 4859 |
[TakeutiZaring] p.
16 | Exercise 8 | rext 4843 |
[TakeutiZaring] p.
16 | Corollary 5.8 | unex 6854 unexg 6857 |
[TakeutiZaring] p.
16 | Definition 5.3 | dftp2 4178 |
[TakeutiZaring] p.
16 | Definition 5.5 | df-uni 4373 |
[TakeutiZaring] p.
16 | Definition 5.6 | df-in 3547 df-un 3545 |
[TakeutiZaring] p.
16 | Proposition 5.7 | unipr 4385 uniprg 4386 |
[TakeutiZaring] p.
17 | Axiom 4 | pwex 4774 pwexg 4776 |
[TakeutiZaring] p.
17 | Exercise 1 | eltp 4177 |
[TakeutiZaring] p.
17 | Exercise 5 | elsuc 5711 elsucg 5709 sstr2 3575 |
[TakeutiZaring] p.
17 | Exercise 6 | uncom 3719 |
[TakeutiZaring] p.
17 | Exercise 7 | incom 3767 |
[TakeutiZaring] p.
17 | Exercise 8 | unass 3732 |
[TakeutiZaring] p.
17 | Exercise 9 | inass 3785 |
[TakeutiZaring] p.
17 | Exercise 10 | indi 3832 |
[TakeutiZaring] p.
17 | Exercise 11 | undi 3833 |
[TakeutiZaring] p.
17 | Definition 5.9 | df-pss 3556 dfss2 3557 |
[TakeutiZaring] p.
17 | Definition 5.10 | df-pw 4110 |
[TakeutiZaring] p.
18 | Exercise 7 | unss2 3746 |
[TakeutiZaring] p.
18 | Exercise 9 | df-ss 3554 sseqin2 3779 |
[TakeutiZaring] p.
18 | Exercise 10 | ssid 3587 |
[TakeutiZaring] p.
18 | Exercise 12 | inss1 3795 inss2 3796 |
[TakeutiZaring] p.
18 | Exercise 13 | nss 3626 |
[TakeutiZaring] p.
18 | Exercise 15 | unieq 4380 |
[TakeutiZaring] p.
18 | Exercise 18 | sspwb 4844 sspwimp 38176 sspwimpALT 38183 sspwimpALT2 38186 sspwimpcf 38178 |
[TakeutiZaring] p.
18 | Exercise 19 | pweqb 4852 |
[TakeutiZaring] p.
19 | Axiom 5 | ax-rep 4699 |
[TakeutiZaring] p.
20 | Definition | df-rab 2905 |
[TakeutiZaring] p.
20 | Corollary 5.16 | 0ex 4718 |
[TakeutiZaring] p.
20 | Definition 5.12 | df-dif 3543 |
[TakeutiZaring] p.
20 | Definition 5.14 | dfnul2 3876 |
[TakeutiZaring] p.
20 | Proposition 5.15 | difid 3902 |
[TakeutiZaring] p.
20 | Proposition 5.17(1) | n0 3890 n0f 3886
neq0 3889 neq0f 3885 |
[TakeutiZaring] p.
21 | Axiom 6 | zfreg 8383 |
[TakeutiZaring] p.
21 | Axiom 6' | zfregs 8491 |
[TakeutiZaring] p.
21 | Theorem 5.22 | setind 8493 |
[TakeutiZaring] p.
21 | Definition 5.20 | df-v 3175 |
[TakeutiZaring] p.
21 | Proposition 5.21 | vprc 4724 |
[TakeutiZaring] p.
22 | Exercise 1 | 0ss 3924 |
[TakeutiZaring] p.
22 | Exercise 3 | ssex 4730 ssexg 4732 |
[TakeutiZaring] p.
22 | Exercise 4 | inex1 4727 |
[TakeutiZaring] p.
22 | Exercise 5 | ruv 8390 |
[TakeutiZaring] p.
22 | Exercise 6 | elirr 8388 |
[TakeutiZaring] p.
22 | Exercise 7 | ssdif0 3896 |
[TakeutiZaring] p.
22 | Exercise 11 | difdif 3698 |
[TakeutiZaring] p.
22 | Exercise 13 | undif3 3847 undif3VD 38140 |
[TakeutiZaring] p.
22 | Exercise 14 | difss 3699 |
[TakeutiZaring] p.
22 | Exercise 15 | sscon 3706 |
[TakeutiZaring] p.
22 | Definition 4.15(3) | df-ral 2901 |
[TakeutiZaring] p.
22 | Definition 4.15(4) | df-rex 2902 |
[TakeutiZaring] p.
23 | Proposition 6.2 | xpex 6860 xpexg 6858 |
[TakeutiZaring] p.
23 | Definition 6.4(1) | df-rel 5045 |
[TakeutiZaring] p.
23 | Definition 6.4(2) | fun2cnv 5874 |
[TakeutiZaring] p.
24 | Definition 6.4(3) | f1cnvcnv 6022 fun11 5877 |
[TakeutiZaring] p.
24 | Definition 6.4(4) | dffun4 5816 svrelfun 5875 |
[TakeutiZaring] p.
24 | Definition 6.5(1) | dfdm3 5232 |
[TakeutiZaring] p.
24 | Definition 6.5(2) | dfrn3 5234 |
[TakeutiZaring] p.
24 | Definition 6.6(1) | df-res 5050 |
[TakeutiZaring] p.
24 | Definition 6.6(2) | df-ima 5051 |
[TakeutiZaring] p.
24 | Definition 6.6(3) | df-co 5047 |
[TakeutiZaring] p.
25 | Exercise 2 | cnvcnvss 5507 dfrel2 5502 |
[TakeutiZaring] p.
25 | Exercise 3 | xpss 5149 |
[TakeutiZaring] p.
25 | Exercise 5 | relun 5158 |
[TakeutiZaring] p.
25 | Exercise 6 | reluni 5164 |
[TakeutiZaring] p.
25 | Exercise 9 | inxp 5176 |
[TakeutiZaring] p.
25 | Exercise 12 | relres 5346 |
[TakeutiZaring] p.
25 | Exercise 13 | opelres 5322 opelresg 5324 |
[TakeutiZaring] p.
25 | Exercise 14 | dmres 5339 |
[TakeutiZaring] p.
25 | Exercise 15 | resss 5342 |
[TakeutiZaring] p.
25 | Exercise 17 | resabs1 5347 |
[TakeutiZaring] p.
25 | Exercise 18 | funres 5843 |
[TakeutiZaring] p.
25 | Exercise 24 | relco 5550 |
[TakeutiZaring] p.
25 | Exercise 29 | funco 5842 |
[TakeutiZaring] p.
25 | Exercise 30 | f1co 6023 |
[TakeutiZaring] p.
26 | Definition 6.10 | eu2 2497 |
[TakeutiZaring] p.
26 | Definition 6.11 | conventions 26650 df-fv 5812 fv3 6116 |
[TakeutiZaring] p.
26 | Corollary 6.8(1) | cnvex 7006 cnvexg 7005 |
[TakeutiZaring] p.
26 | Corollary 6.8(2) | dmex 6991 dmexg 6989 |
[TakeutiZaring] p.
26 | Corollary 6.8(3) | rnex 6992 rnexg 6990 |
[TakeutiZaring] p. 26 | Corollary
6.9(1) | xpexb 37679 |
[TakeutiZaring] p.
26 | Corollary 6.9(2) | xpexcnv 7001 |
[TakeutiZaring] p.
27 | Corollary 6.13 | fvex 6113 |
[TakeutiZaring] p. 27 | Theorem
6.12(1) | tz6.12-1-afv 39903 tz6.12-1 6120 tz6.12-afv 39902 tz6.12 6121 tz6.12c 6123 |
[TakeutiZaring] p.
27 | Theorem 6.12(2) | tz6.12-2 6094 tz6.12i 6124 |
[TakeutiZaring] p.
27 | Definition 6.15(1) | df-fn 5807 |
[TakeutiZaring] p.
27 | Definition 6.15(3) | df-f 5808 |
[TakeutiZaring] p.
27 | Definition 6.15(4) | df-fo 5810 wfo 5802 |
[TakeutiZaring] p.
27 | Definition 6.15(5) | df-f1 5809 wf1 5801 |
[TakeutiZaring] p.
27 | Definition 6.15(6) | df-f1o 5811 wf1o 5803 |
[TakeutiZaring] p.
28 | Exercise 4 | eqfnfv 6219 eqfnfv2 6220 eqfnfv2f 6223 |
[TakeutiZaring] p.
28 | Exercise 5 | fvco 6184 |
[TakeutiZaring] p.
28 | Theorem 6.16(1) | fnex 6386 |
[TakeutiZaring] p.
28 | Proposition 6.17 | resfunexg 6384 |
[TakeutiZaring] p.
29 | Exercise 9 | funimaex 5890 funimaexg 5889 |
[TakeutiZaring] p.
29 | Definition 6.18 | df-br 4584 |
[TakeutiZaring] p.
29 | Definition 6.19(1) | df-so 4960 |
[TakeutiZaring] p.
30 | Definition 6.21 | dffr2 5003 dffr3 5417 eliniseg 5413 iniseg 5415 |
[TakeutiZaring] p.
30 | Definition 6.22 | df-eprel 4949 |
[TakeutiZaring] p.
30 | Proposition 6.23 | fr2nr 5016 fr3nr 6871 frirr 5015 |
[TakeutiZaring] p.
30 | Definition 6.24(1) | df-fr 4997 |
[TakeutiZaring] p.
30 | Definition 6.24(2) | dfwe2 6873 |
[TakeutiZaring] p.
31 | Exercise 1 | frss 5005 |
[TakeutiZaring] p.
31 | Exercise 4 | wess 5025 |
[TakeutiZaring] p.
31 | Proposition 6.26 | tz6.26 5628 tz6.26i 5629 wefrc 5032 wereu2 5035 |
[TakeutiZaring] p.
32 | Theorem 6.27 | wfi 5630 wfii 5631 |
[TakeutiZaring] p.
32 | Definition 6.28 | df-isom 5813 |
[TakeutiZaring] p.
33 | Proposition 6.30(1) | isoid 6479 |
[TakeutiZaring] p.
33 | Proposition 6.30(2) | isocnv 6480 |
[TakeutiZaring] p.
33 | Proposition 6.30(3) | isotr 6486 |
[TakeutiZaring] p.
33 | Proposition 6.31(1) | isomin 6487 |
[TakeutiZaring] p.
33 | Proposition 6.31(2) | isoini 6488 |
[TakeutiZaring] p.
33 | Proposition 6.32(1) | isofr 6492 |
[TakeutiZaring] p.
33 | Proposition 6.32(3) | isowe 6499 |
[TakeutiZaring] p.
34 | Proposition 6.33 | f1oiso 6501 |
[TakeutiZaring] p.
35 | Notation | wtr 4680 |
[TakeutiZaring] p. 35 | Theorem
7.2 | trelpss 37680 tz7.2 5022 |
[TakeutiZaring] p.
35 | Definition 7.1 | dftr3 4684 |
[TakeutiZaring] p.
36 | Proposition 7.4 | ordwe 5653 |
[TakeutiZaring] p.
36 | Proposition 7.5 | tz7.5 5661 |
[TakeutiZaring] p.
36 | Proposition 7.6 | ordelord 5662 ordelordALT 37768 ordelordALTVD 38125 |
[TakeutiZaring] p.
37 | Corollary 7.8 | ordelpss 5668 ordelssne 5667 |
[TakeutiZaring] p.
37 | Proposition 7.7 | tz7.7 5666 |
[TakeutiZaring] p.
37 | Proposition 7.9 | ordin 5670 |
[TakeutiZaring] p.
38 | Corollary 7.14 | ordeleqon 6880 |
[TakeutiZaring] p.
38 | Corollary 7.15 | ordsson 6881 |
[TakeutiZaring] p.
38 | Definition 7.11 | df-on 5644 |
[TakeutiZaring] p.
38 | Proposition 7.10 | ordtri3or 5672 |
[TakeutiZaring] p. 38 | Proposition
7.12 | onfrALT 37785 ordon 6874 |
[TakeutiZaring] p.
38 | Proposition 7.13 | onprc 6876 |
[TakeutiZaring] p.
39 | Theorem 7.17 | tfi 6945 |
[TakeutiZaring] p.
40 | Exercise 3 | ontr2 5689 |
[TakeutiZaring] p.
40 | Exercise 7 | dftr2 4682 |
[TakeutiZaring] p.
40 | Exercise 9 | onssmin 6889 |
[TakeutiZaring] p.
40 | Exercise 11 | unon 6923 |
[TakeutiZaring] p.
40 | Exercise 12 | ordun 5746 |
[TakeutiZaring] p.
40 | Exercise 14 | ordequn 5745 |
[TakeutiZaring] p.
40 | Proposition 7.19 | ssorduni 6877 |
[TakeutiZaring] p.
40 | Proposition 7.20 | elssuni 4403 |
[TakeutiZaring] p.
41 | Definition 7.22 | df-suc 5646 |
[TakeutiZaring] p.
41 | Proposition 7.23 | sssucid 5719 sucidg 5720 |
[TakeutiZaring] p.
41 | Proposition 7.24 | suceloni 6905 |
[TakeutiZaring] p.
41 | Proposition 7.25 | onnbtwn 5735 ordnbtwn 5733 |
[TakeutiZaring] p.
41 | Proposition 7.26 | onsucuni 6920 |
[TakeutiZaring] p.
42 | Exercise 1 | df-lim 5645 |
[TakeutiZaring] p.
42 | Exercise 4 | omssnlim 6971 |
[TakeutiZaring] p.
42 | Exercise 7 | ssnlim 6975 |
[TakeutiZaring] p.
42 | Exercise 8 | onsucssi 6933 ordelsuc 6912 |
[TakeutiZaring] p.
42 | Exercise 9 | ordsucelsuc 6914 |
[TakeutiZaring] p.
42 | Definition 7.27 | nlimon 6943 |
[TakeutiZaring] p.
42 | Definition 7.28 | dfom2 6959 |
[TakeutiZaring] p.
42 | Proposition 7.30(1) | peano1 6977 |
[TakeutiZaring] p.
42 | Proposition 7.30(2) | peano2 6978 |
[TakeutiZaring] p.
42 | Proposition 7.30(3) | peano3 6979 |
[TakeutiZaring] p.
43 | Remark | omon 6968 |
[TakeutiZaring] p.
43 | Axiom 7 | inf3 8415 omex 8423 |
[TakeutiZaring] p.
43 | Theorem 7.32 | ordom 6966 |
[TakeutiZaring] p.
43 | Corollary 7.31 | find 6983 |
[TakeutiZaring] p.
43 | Proposition 7.30(4) | peano4 6980 |
[TakeutiZaring] p.
43 | Proposition 7.30(5) | peano5 6981 |
[TakeutiZaring] p.
44 | Exercise 1 | limomss 6962 |
[TakeutiZaring] p.
44 | Exercise 2 | int0 4425 trint0 4698 |
[TakeutiZaring] p.
44 | Exercise 4 | intss1 4427 |
[TakeutiZaring] p.
44 | Exercise 5 | intex 4747 |
[TakeutiZaring] p.
44 | Exercise 6 | oninton 6892 |
[TakeutiZaring] p.
44 | Exercise 11 | ordintdif 5691 |
[TakeutiZaring] p.
44 | Definition 7.35 | df-int 4411 |
[TakeutiZaring] p.
44 | Proposition 7.34 | noinfep 8440 |
[TakeutiZaring] p.
45 | Exercise 4 | onint 6887 |
[TakeutiZaring] p.
47 | Lemma 1 | tfrlem1 7359 |
[TakeutiZaring] p.
47 | Theorem 7.41(1) | tfr1 7380 |
[TakeutiZaring] p.
47 | Theorem 7.41(2) | tfr2 7381 |
[TakeutiZaring] p.
47 | Theorem 7.41(3) | tfr3 7382 |
[TakeutiZaring] p.
49 | Theorem 7.44 | tz7.44-1 7389 tz7.44-2 7390 tz7.44-3 7391 |
[TakeutiZaring] p.
50 | Exercise 1 | smogt 7351 |
[TakeutiZaring] p.
50 | Exercise 3 | smoiso 7346 |
[TakeutiZaring] p.
50 | Definition 7.46 | df-smo 7330 |
[TakeutiZaring] p.
51 | Proposition 7.49 | tz7.49 7427 tz7.49c 7428 |
[TakeutiZaring] p.
51 | Proposition 7.48(1) | tz7.48-1 7425 |
[TakeutiZaring] p.
51 | Proposition 7.48(2) | tz7.48-2 7424 |
[TakeutiZaring] p.
51 | Proposition 7.48(3) | tz7.48-3 7426 |
[TakeutiZaring] p.
53 | Proposition 7.53 | 2eu5 2545 |
[TakeutiZaring] p.
54 | Proposition 7.56(1) | leweon 8717 |
[TakeutiZaring] p.
54 | Proposition 7.58(1) | r0weon 8718 |
[TakeutiZaring] p.
56 | Definition 8.1 | oalim 7499 oasuc 7491 |
[TakeutiZaring] p.
57 | Remark | tfindsg 6952 |
[TakeutiZaring] p.
57 | Proposition 8.2 | oacl 7502 |
[TakeutiZaring] p.
57 | Proposition 8.3 | oa0 7483 oa0r 7505 |
[TakeutiZaring] p.
57 | Proposition 8.16 | omcl 7503 |
[TakeutiZaring] p.
58 | Corollary 8.5 | oacan 7515 |
[TakeutiZaring] p.
58 | Proposition 8.4 | nnaord 7586 nnaordi 7585 oaord 7514 oaordi 7513 |
[TakeutiZaring] p.
59 | Proposition 8.6 | iunss2 4501 uniss2 4406 |
[TakeutiZaring] p.
59 | Proposition 8.7 | oawordri 7517 |
[TakeutiZaring] p.
59 | Proposition 8.8 | oawordeu 7522 oawordex 7524 |
[TakeutiZaring] p.
59 | Proposition 8.9 | nnacl 7578 |
[TakeutiZaring] p.
59 | Proposition 8.10 | oaabs 7611 |
[TakeutiZaring] p.
60 | Remark | oancom 8431 |
[TakeutiZaring] p.
60 | Proposition 8.11 | oalimcl 7527 |
[TakeutiZaring] p.
62 | Exercise 1 | nnarcl 7583 |
[TakeutiZaring] p.
62 | Exercise 5 | oaword1 7519 |
[TakeutiZaring] p.
62 | Definition 8.15 | om0 7484 om0x 7486
omlim 7500 omsuc 7493 |
[TakeutiZaring] p.
63 | Proposition 8.17 | nnecl 7580 nnmcl 7579 |
[TakeutiZaring] p.
63 | Proposition 8.19 | nnmord 7599 nnmordi 7598 omord 7535 omordi 7533 |
[TakeutiZaring] p.
63 | Proposition 8.20 | omcan 7536 |
[TakeutiZaring] p.
63 | Proposition 8.21 | nnmwordri 7603 omwordri 7539 |
[TakeutiZaring] p.
63 | Proposition 8.18(1) | om0r 7506 |
[TakeutiZaring] p.
63 | Proposition 8.18(2) | om1 7509 om1r 7510 |
[TakeutiZaring] p.
64 | Proposition 8.22 | om00 7542 |
[TakeutiZaring] p.
64 | Proposition 8.23 | omordlim 7544 |
[TakeutiZaring] p.
64 | Proposition 8.24 | omlimcl 7545 |
[TakeutiZaring] p.
64 | Proposition 8.25 | odi 7546 |
[TakeutiZaring] p.
65 | Theorem 8.26 | omass 7547 |
[TakeutiZaring] p.
67 | Definition 8.30 | nnesuc 7575 oe0 7489
oelim 7501 oesuc 7494 onesuc 7497 |
[TakeutiZaring] p.
67 | Proposition 8.31 | oe0m0 7487 |
[TakeutiZaring] p.
67 | Proposition 8.32 | oen0 7553 |
[TakeutiZaring] p.
67 | Proposition 8.33 | oeordi 7554 |
[TakeutiZaring] p.
67 | Proposition 8.31(2) | oe0m1 7488 |
[TakeutiZaring] p.
67 | Proposition 8.31(3) | oe1m 7512 |
[TakeutiZaring] p.
68 | Corollary 8.34 | oeord 7555 |
[TakeutiZaring] p.
68 | Corollary 8.36 | oeordsuc 7561 |
[TakeutiZaring] p.
68 | Proposition 8.35 | oewordri 7559 |
[TakeutiZaring] p.
68 | Proposition 8.37 | oeworde 7560 |
[TakeutiZaring] p.
69 | Proposition 8.41 | oeoa 7564 |
[TakeutiZaring] p.
70 | Proposition 8.42 | oeoe 7566 |
[TakeutiZaring] p.
73 | Theorem 9.1 | trcl 8487 tz9.1 8488 |
[TakeutiZaring] p.
76 | Definition 9.9 | df-r1 8510 r10 8514
r1lim 8518 r1limg 8517 r1suc 8516 r1sucg 8515 |
[TakeutiZaring] p.
77 | Proposition 9.10(2) | r1ord 8526 r1ord2 8527 r1ordg 8524 |
[TakeutiZaring] p.
78 | Proposition 9.12 | tz9.12 8536 |
[TakeutiZaring] p.
78 | Proposition 9.13 | rankwflem 8561 tz9.13 8537 tz9.13g 8538 |
[TakeutiZaring] p.
79 | Definition 9.14 | df-rank 8511 rankval 8562 rankvalb 8543 rankvalg 8563 |
[TakeutiZaring] p.
79 | Proposition 9.16 | rankel 8585 rankelb 8570 |
[TakeutiZaring] p.
79 | Proposition 9.17 | rankuni2b 8599 rankval3 8586 rankval3b 8572 |
[TakeutiZaring] p.
79 | Proposition 9.18 | rankonid 8575 |
[TakeutiZaring] p.
79 | Proposition 9.15(1) | rankon 8541 |
[TakeutiZaring] p.
79 | Proposition 9.15(2) | rankr1 8580 rankr1c 8567 rankr1g 8578 |
[TakeutiZaring] p.
79 | Proposition 9.15(3) | ssrankr1 8581 |
[TakeutiZaring] p.
80 | Exercise 1 | rankss 8595 rankssb 8594 |
[TakeutiZaring] p.
80 | Exercise 2 | unbndrank 8588 |
[TakeutiZaring] p.
80 | Proposition 9.19 | bndrank 8587 |
[TakeutiZaring] p.
83 | Axiom of Choice | ac4 9180 dfac3 8827 |
[TakeutiZaring] p.
84 | Theorem 10.3 | dfac8a 8736 numth 9177 numth2 9176 |
[TakeutiZaring] p.
85 | Definition 10.4 | cardval 9247 |
[TakeutiZaring] p.
85 | Proposition 10.5 | cardid 9248 cardid2 8662 |
[TakeutiZaring] p.
85 | Proposition 10.9 | oncard 8669 |
[TakeutiZaring] p.
85 | Proposition 10.10 | carden 9252 |
[TakeutiZaring] p.
85 | Proposition 10.11 | cardidm 8668 |
[TakeutiZaring] p.
85 | Proposition 10.6(1) | cardon 8653 |
[TakeutiZaring] p.
85 | Proposition 10.6(2) | cardne 8674 |
[TakeutiZaring] p.
85 | Proposition 10.6(3) | cardonle 8666 |
[TakeutiZaring] p.
87 | Proposition 10.15 | pwen 8018 |
[TakeutiZaring] p.
88 | Exercise 1 | en0 7905 |
[TakeutiZaring] p.
88 | Exercise 7 | infensuc 8023 |
[TakeutiZaring] p.
89 | Exercise 10 | omxpen 7947 |
[TakeutiZaring] p.
90 | Corollary 10.23 | cardnn 8672 |
[TakeutiZaring] p.
90 | Definition 10.27 | alephiso 8804 |
[TakeutiZaring] p.
90 | Proposition 10.20 | nneneq 8028 |
[TakeutiZaring] p.
90 | Proposition 10.22 | onomeneq 8035 |
[TakeutiZaring] p.
90 | Proposition 10.26 | alephprc 8805 |
[TakeutiZaring] p.
90 | Corollary 10.21(1) | php5 8033 |
[TakeutiZaring] p.
91 | Exercise 2 | alephle 8794 |
[TakeutiZaring] p.
91 | Exercise 3 | aleph0 8772 |
[TakeutiZaring] p.
91 | Exercise 4 | cardlim 8681 |
[TakeutiZaring] p.
91 | Exercise 7 | infpss 8922 |
[TakeutiZaring] p.
91 | Exercise 8 | infcntss 8119 |
[TakeutiZaring] p.
91 | Definition 10.29 | df-fin 7845 isfi 7865 |
[TakeutiZaring] p.
92 | Proposition 10.32 | onfin 8036 |
[TakeutiZaring] p.
92 | Proposition 10.34 | imadomg 9237 |
[TakeutiZaring] p.
92 | Proposition 10.33(2) | xpdom2 7940 |
[TakeutiZaring] p.
93 | Proposition 10.35 | fodomb 9229 |
[TakeutiZaring] p.
93 | Proposition 10.36 | cdaxpdom 8894 unxpdom 8052 |
[TakeutiZaring] p.
93 | Proposition 10.37 | cardsdomel 8683 cardsdomelir 8682 |
[TakeutiZaring] p.
93 | Proposition 10.38 | sucxpdom 8054 |
[TakeutiZaring] p.
94 | Proposition 10.39 | infxpen 8720 |
[TakeutiZaring] p.
95 | Definition 10.42 | df-map 7746 |
[TakeutiZaring] p.
95 | Proposition 10.40 | infxpidm 9263 infxpidm2 8723 |
[TakeutiZaring] p.
95 | Proposition 10.41 | infcda 8913 infxp 8920 |
[TakeutiZaring] p.
96 | Proposition 10.44 | pw2en 7952 pw2f1o 7950 |
[TakeutiZaring] p.
96 | Proposition 10.45 | mapxpen 8011 |
[TakeutiZaring] p.
97 | Theorem 10.46 | ac6s3 9192 |
[TakeutiZaring] p.
98 | Theorem 10.46 | ac6c5 9187 ac6s5 9196 |
[TakeutiZaring] p.
98 | Theorem 10.47 | unidom 9244 |
[TakeutiZaring] p.
99 | Theorem 10.48 | uniimadom 9245 uniimadomf 9246 |
[TakeutiZaring] p.
100 | Definition 11.1 | cfcof 8979 |
[TakeutiZaring] p.
101 | Proposition 11.7 | cofsmo 8974 |
[TakeutiZaring] p.
102 | Exercise 1 | cfle 8959 |
[TakeutiZaring] p.
102 | Exercise 2 | cf0 8956 |
[TakeutiZaring] p.
102 | Exercise 3 | cfsuc 8962 |
[TakeutiZaring] p.
102 | Exercise 4 | cfom 8969 |
[TakeutiZaring] p.
102 | Proposition 11.9 | coftr 8978 |
[TakeutiZaring] p.
103 | Theorem 11.15 | alephreg 9283 |
[TakeutiZaring] p.
103 | Proposition 11.11 | cardcf 8957 |
[TakeutiZaring] p.
103 | Proposition 11.13 | alephsing 8981 |
[TakeutiZaring] p.
104 | Corollary 11.17 | cardinfima 8803 |
[TakeutiZaring] p.
104 | Proposition 11.16 | carduniima 8802 |
[TakeutiZaring] p.
104 | Proposition 11.18 | alephfp 8814 alephfp2 8815 |
[TakeutiZaring] p.
106 | Theorem 11.20 | gchina 9400 |
[TakeutiZaring] p.
106 | Theorem 11.21 | mappwen 8818 |
[TakeutiZaring] p.
107 | Theorem 11.26 | konigth 9270 |
[TakeutiZaring] p.
108 | Theorem 11.28 | pwcfsdom 9284 |
[TakeutiZaring] p.
108 | Theorem 11.29 | cfpwsdom 9285 |
[Tarski] p.
67 | Axiom B5 | ax-c5 33186 |
[Tarski] p. 67 | Scheme
B5 | sp 2041 |
[Tarski] p. 68 | Lemma
6 | avril1 26711 equid 1926 |
[Tarski] p. 69 | Lemma
7 | equcomi 1931 |
[Tarski] p. 70 | Lemma
14 | spim 2242 spime 2244 spimeh 1912 |
[Tarski] p. 70 | Lemma
16 | ax-12 2034 ax-c15 33192 ax12i 1866 |
[Tarski] p. 70 | Lemmas 16
and 17 | sb6 2417 |
[Tarski] p. 75 | Axiom
B7 | ax6v 1876 |
[Tarski] p. 77 | Axiom B6
(p. 75) of system S2 | ax-5 1827 ax5ALT 33210 |
[Tarski], p. 75 | Scheme
B8 of system S2 | ax-7 1922 ax-8 1979
ax-9 1986 |
[Tarski1999] p.
178 | Axiom 4 | axtgsegcon 25163 |
[Tarski1999] p.
178 | Axiom 5 | axtg5seg 25164 |
[Tarski1999] p.
179 | Axiom 7 | axtgpasch 25166 |
[Tarski1999] p.
180 | Axiom 7.1 | axtgpasch 25166 |
[Tarski1999] p.
185 | Axiom 11 | axtgcont1 25167 |
[Truss] p. 114 | Theorem
5.18 | ruc 14811 |
[Viaclovsky7] p. 3 | Corollary
0.3 | mblfinlem3 32618 |
[Viaclovsky8] p. 3 | Proposition
7 | ismblfin 32620 |
[Weierstrass] p.
272 | Definition | df-mdet 20210 mdetuni 20247 |
[WhiteheadRussell] p.
96 | Axiom *1.2 | pm1.2 534 |
[WhiteheadRussell] p.
96 | Axiom *1.3 | olc 398 |
[WhiteheadRussell] p.
96 | Axiom *1.4 | pm1.4 400 |
[WhiteheadRussell] p.
96 | Axiom *1.5 (Assoc) | pm1.5 543 |
[WhiteheadRussell] p.
97 | Axiom *1.6 (Sum) | orim2 882 |
[WhiteheadRussell] p.
100 | Theorem *2.01 | pm2.01 179 |
[WhiteheadRussell] p.
100 | Theorem *2.02 | ax-1 6 |
[WhiteheadRussell] p.
100 | Theorem *2.03 | con2 129 |
[WhiteheadRussell] p.
100 | Theorem *2.04 | pm2.04 88 wl-pm2.04 32443 |
[WhiteheadRussell] p.
100 | Theorem *2.05 | frege5 37114 imim2 56
wl-imim2 32438 |
[WhiteheadRussell] p.
100 | Theorem *2.06 | imim1 81 |
[WhiteheadRussell] p.
101 | Theorem *2.1 | pm2.1 432 |
[WhiteheadRussell] p.
101 | Theorem *2.06 | barbara 2551 syl 17 |
[WhiteheadRussell] p.
101 | Theorem *2.07 | pm2.07 410 |
[WhiteheadRussell] p.
101 | Theorem *2.08 | id 22 wl-id 32441 |
[WhiteheadRussell] p.
101 | Theorem *2.11 | exmid 430 |
[WhiteheadRussell] p.
101 | Theorem *2.12 | notnot 135 |
[WhiteheadRussell] p.
101 | Theorem *2.13 | pm2.13 433 |
[WhiteheadRussell] p.
102 | Theorem *2.14 | notnotr 124 notnotrALT2 38185 wl-notnotr 32442 |
[WhiteheadRussell] p.
102 | Theorem *2.15 | con1 142 |
[WhiteheadRussell] p.
103 | Theorem *2.16 | ax-frege28 37144 axfrege28 37143 con3 148 |
[WhiteheadRussell] p.
103 | Theorem *2.17 | ax-3 8 |
[WhiteheadRussell] p.
103 | Theorem *2.18 | pm2.18 121 |
[WhiteheadRussell] p.
104 | Theorem *2.2 | orc 399 |
[WhiteheadRussell] p.
104 | Theorem *2.3 | pm2.3 594 |
[WhiteheadRussell] p.
104 | Theorem *2.21 | pm2.21 119 wl-pm2.21 32435 |
[WhiteheadRussell] p.
104 | Theorem *2.24 | pm2.24 120 |
[WhiteheadRussell] p.
104 | Theorem *2.25 | pm2.25 418 |
[WhiteheadRussell] p.
104 | Theorem *2.26 | pm2.26 923 |
[WhiteheadRussell] p.
104 | Theorem *2.27 | conventions-label 26651 pm2.27 41 wl-pm2.27 32433 |
[WhiteheadRussell] p.
104 | Theorem *2.31 | pm2.31 546 |
[WhiteheadRussell] p.
105 | Theorem *2.32 | pm2.32 547 |
[WhiteheadRussell] p.
105 | Theorem *2.36 | pm2.36 884 |
[WhiteheadRussell] p.
105 | Theorem *2.37 | pm2.37 885 |
[WhiteheadRussell] p.
105 | Theorem *2.38 | pm2.38 883 |
[WhiteheadRussell] p.
105 | Definition *2.33 | df-3or 1032 |
[WhiteheadRussell] p.
106 | Theorem *2.4 | pm2.4 597 |
[WhiteheadRussell] p.
106 | Theorem *2.41 | pm2.41 595 |
[WhiteheadRussell] p.
106 | Theorem *2.42 | pm2.42 596 |
[WhiteheadRussell] p.
106 | Theorem *2.43 | pm2.43 54 |
[WhiteheadRussell] p.
106 | Theorem *2.45 | pm2.45 411 |
[WhiteheadRussell] p.
106 | Theorem *2.46 | pm2.46 412 |
[WhiteheadRussell] p.
107 | Theorem *2.5 | pm2.5 163 |
[WhiteheadRussell] p.
107 | Theorem *2.6 | pm2.6 181 |
[WhiteheadRussell] p.
107 | Theorem *2.47 | pm2.47 413 |
[WhiteheadRussell] p.
107 | Theorem *2.48 | pm2.48 414 |
[WhiteheadRussell] p.
107 | Theorem *2.49 | pm2.49 415 |
[WhiteheadRussell] p.
107 | Theorem *2.51 | pm2.51 164 |
[WhiteheadRussell] p.
107 | Theorem *2.52 | pm2.52 166 |
[WhiteheadRussell] p.
107 | Theorem *2.53 | pm2.53 387 |
[WhiteheadRussell] p.
107 | Theorem *2.54 | pm2.54 388 |
[WhiteheadRussell] p.
107 | Theorem *2.55 | orel1 396 |
[WhiteheadRussell] p.
107 | Theorem *2.56 | orel2 397 |
[WhiteheadRussell] p.
107 | Theorem *2.61 | pm2.61 182 |
[WhiteheadRussell] p.
107 | Theorem *2.62 | pm2.62 424 |
[WhiteheadRussell] p.
107 | Theorem *2.63 | pm2.63 825 |
[WhiteheadRussell] p.
107 | Theorem *2.64 | pm2.64 826 |
[WhiteheadRussell] p.
107 | Theorem *2.65 | pm2.65 183 |
[WhiteheadRussell] p.
107 | Theorem *2.67 | pm2.67-2 416 pm2.67 417 |
[WhiteheadRussell] p.
107 | Theorem *2.521 | pm2.521 165 |
[WhiteheadRussell] p.
107 | Theorem *2.621 | pm2.621 423 |
[WhiteheadRussell] p.
108 | Theorem *2.8 | pm2.8 891 |
[WhiteheadRussell] p.
108 | Theorem *2.68 | pm2.68 425 |
[WhiteheadRussell] p.
108 | Theorem *2.69 | looinv 193 |
[WhiteheadRussell] p.
108 | Theorem *2.73 | pm2.73 886 |
[WhiteheadRussell] p.
108 | Theorem *2.74 | pm2.74 887 |
[WhiteheadRussell] p.
108 | Theorem *2.75 | pm2.75 890 |
[WhiteheadRussell] p.
108 | Theorem *2.76 | pm2.76 889 |
[WhiteheadRussell] p.
108 | Theorem *2.77 | ax-2 7 |
[WhiteheadRussell] p.
108 | Theorem *2.81 | pm2.81 892 |
[WhiteheadRussell] p.
108 | Theorem *2.82 | pm2.82 893 |
[WhiteheadRussell] p.
108 | Theorem *2.83 | pm2.83 82 |
[WhiteheadRussell] p.
108 | Theorem *2.85 | pm2.85 894 |
[WhiteheadRussell] p.
108 | Theorem *2.86 | pm2.86 106 |
[WhiteheadRussell] p.
111 | Theorem *3.1 | pm3.1 518 |
[WhiteheadRussell] p.
111 | Theorem *3.2 | pm3.2 462 pm3.2im 156 |
[WhiteheadRussell] p.
111 | Theorem *3.11 | pm3.11 519 |
[WhiteheadRussell] p.
111 | Theorem *3.12 | pm3.12 520 |
[WhiteheadRussell] p.
111 | Theorem *3.13 | pm3.13 521 |
[WhiteheadRussell] p.
111 | Theorem *3.14 | pm3.14 522 |
[WhiteheadRussell] p.
111 | Theorem *3.21 | pm3.21 463 |
[WhiteheadRussell] p.
111 | Theorem *3.22 | pm3.22 464 |
[WhiteheadRussell] p.
111 | Theorem *3.24 | pm3.24 922 |
[WhiteheadRussell] p.
112 | Theorem *3.35 | pm3.35 609 |
[WhiteheadRussell] p.
112 | Theorem *3.3 (Exp) | pm3.3 459 |
[WhiteheadRussell] p.
112 | Theorem *3.31 (Imp) | pm3.31 460 |
[WhiteheadRussell] p.
112 | Theorem *3.26 (Simp) | simpl 472 simplim 162 |
[WhiteheadRussell] p.
112 | Theorem *3.27 (Simp) | simpr 476 simprim 161 |
[WhiteheadRussell] p.
112 | Theorem *3.33 (Syll) | pm3.33 607 |
[WhiteheadRussell] p.
112 | Theorem *3.34 (Syll) | pm3.34 608 |
[WhiteheadRussell] p.
112 | Theorem *3.37 (Transp) | pm3.37 601 |
[WhiteheadRussell] p.
113 | Fact) | pm3.45 875 |
[WhiteheadRussell] p.
113 | Theorem *3.4 | pm3.4 582 |
[WhiteheadRussell] p.
113 | Theorem *3.41 | pm3.41 580 |
[WhiteheadRussell] p.
113 | Theorem *3.42 | pm3.42 581 |
[WhiteheadRussell] p.
113 | Theorem *3.44 | jao 533 pm3.44 532 |
[WhiteheadRussell] p.
113 | Theorem *3.47 | prth 593 |
[WhiteheadRussell] p.
113 | Theorem *3.43 (Comp) | pm3.43 902 |
[WhiteheadRussell] p.
114 | Theorem *3.48 | pm3.48 874 |
[WhiteheadRussell] p.
116 | Theorem *4.1 | con34b 305 |
[WhiteheadRussell] p.
117 | Theorem *4.2 | biid 250 |
[WhiteheadRussell] p.
117 | Theorem *4.11 | notbi 308 |
[WhiteheadRussell] p.
117 | Theorem *4.12 | con2bi 342 |
[WhiteheadRussell] p.
117 | Theorem *4.13 | notnotb 303 |
[WhiteheadRussell] p.
117 | Theorem *4.14 | pm4.14 600 |
[WhiteheadRussell] p.
117 | Theorem *4.15 | pm4.15 603 |
[WhiteheadRussell] p.
117 | Theorem *4.21 | bicom 211 |
[WhiteheadRussell] p.
117 | Theorem *4.22 | biantr 968 bitr 741 |
[WhiteheadRussell] p.
117 | Theorem *4.24 | pm4.24 673 |
[WhiteheadRussell] p.
117 | Theorem *4.25 | oridm 535 pm4.25 536 |
[WhiteheadRussell] p.
118 | Theorem *4.3 | ancom 465 |
[WhiteheadRussell] p.
118 | Theorem *4.4 | andi 907 |
[WhiteheadRussell] p.
118 | Theorem *4.31 | orcom 401 |
[WhiteheadRussell] p.
118 | Theorem *4.32 | anass 679 |
[WhiteheadRussell] p.
118 | Theorem *4.33 | orass 545 |
[WhiteheadRussell] p.
118 | Theorem *4.36 | anbi1 739 |
[WhiteheadRussell] p.
118 | Theorem *4.37 | orbi1 738 |
[WhiteheadRussell] p.
118 | Theorem *4.38 | pm4.38 912 |
[WhiteheadRussell] p.
118 | Theorem *4.39 | pm4.39 911 |
[WhiteheadRussell] p.
118 | Definition *4.34 | df-3an 1033 |
[WhiteheadRussell] p.
119 | Theorem *4.41 | ordi 904 |
[WhiteheadRussell] p.
119 | Theorem *4.42 | pm4.42 995 |
[WhiteheadRussell] p.
119 | Theorem *4.43 | pm4.43 964 |
[WhiteheadRussell] p.
119 | Theorem *4.44 | pm4.44 599 |
[WhiteheadRussell] p.
119 | Theorem *4.45 | orabs 896 pm4.45 720 pm4.45im 583 |
[WhiteheadRussell] p.
120 | Theorem *4.5 | anor 509 |
[WhiteheadRussell] p.
120 | Theorem *4.6 | imor 427 |
[WhiteheadRussell] p.
120 | Theorem *4.7 | anclb 568 |
[WhiteheadRussell] p.
120 | Theorem *4.51 | ianor 508 |
[WhiteheadRussell] p.
120 | Theorem *4.52 | pm4.52 511 |
[WhiteheadRussell] p.
120 | Theorem *4.53 | pm4.53 512 |
[WhiteheadRussell] p.
120 | Theorem *4.54 | pm4.54 513 |
[WhiteheadRussell] p.
120 | Theorem *4.55 | pm4.55 514 |
[WhiteheadRussell] p.
120 | Theorem *4.56 | ioran 510 pm4.56 515 |
[WhiteheadRussell] p.
120 | Theorem *4.57 | oran 516 pm4.57 517 |
[WhiteheadRussell] p.
120 | Theorem *4.61 | pm4.61 441 |
[WhiteheadRussell] p.
120 | Theorem *4.62 | pm4.62 434 |
[WhiteheadRussell] p.
120 | Theorem *4.63 | pm4.63 436 |
[WhiteheadRussell] p.
120 | Theorem *4.64 | pm4.64 386 |
[WhiteheadRussell] p.
120 | Theorem *4.65 | pm4.65 442 |
[WhiteheadRussell] p.
120 | Theorem *4.66 | pm4.66 435 |
[WhiteheadRussell] p.
120 | Theorem *4.67 | pm4.67 443 |
[WhiteheadRussell] p.
120 | Theorem *4.71 | pm4.71 660 pm4.71d 664 pm4.71i 662 pm4.71r 661 pm4.71rd 665 pm4.71ri 663 |
[WhiteheadRussell] p.
121 | Theorem *4.72 | pm4.72 916 |
[WhiteheadRussell] p.
121 | Theorem *4.73 | iba 523 |
[WhiteheadRussell] p.
121 | Theorem *4.74 | biorf 419 |
[WhiteheadRussell] p.
121 | Theorem *4.76 | jcab 903 pm4.76 906 |
[WhiteheadRussell] p.
121 | Theorem *4.77 | jaob 818 pm4.77 824 |
[WhiteheadRussell] p.
121 | Theorem *4.78 | pm4.78 604 |
[WhiteheadRussell] p.
121 | Theorem *4.79 | pm4.79 605 |
[WhiteheadRussell] p.
122 | Theorem *4.8 | pm4.8 379 |
[WhiteheadRussell] p.
122 | Theorem *4.81 | pm4.81 380 |
[WhiteheadRussell] p.
122 | Theorem *4.82 | pm4.82 965 |
[WhiteheadRussell] p.
122 | Theorem *4.83 | pm4.83 966 |
[WhiteheadRussell] p.
122 | Theorem *4.84 | imbi1 336 |
[WhiteheadRussell] p.
122 | Theorem *4.85 | imbi2 337 |
[WhiteheadRussell] p.
122 | Theorem *4.86 | bibi1 340 |
[WhiteheadRussell] p.
122 | Theorem *4.87 | bi2.04 375 impexp 461 pm4.87 606 |
[WhiteheadRussell] p.
123 | Theorem *5.1 | pm5.1 898 |
[WhiteheadRussell] p.
123 | Theorem *5.11 | pm5.11 924 |
[WhiteheadRussell] p.
123 | Theorem *5.12 | pm5.12 925 |
[WhiteheadRussell] p.
123 | Theorem *5.13 | pm5.13 927 |
[WhiteheadRussell] p.
123 | Theorem *5.14 | pm5.14 926 |
[WhiteheadRussell] p.
124 | Theorem *5.15 | pm5.15 929 |
[WhiteheadRussell] p.
124 | Theorem *5.16 | pm5.16 930 |
[WhiteheadRussell] p.
124 | Theorem *5.17 | pm5.17 928 |
[WhiteheadRussell] p.
124 | Theorem *5.18 | nbbn 372 pm5.18 370 |
[WhiteheadRussell] p.
124 | Theorem *5.19 | pm5.19 374 |
[WhiteheadRussell] p.
124 | Theorem *5.21 | pm5.21 899 |
[WhiteheadRussell] p.
124 | Theorem *5.22 | xor 931 |
[WhiteheadRussell] p.
124 | Theorem *5.23 | dfbi3 933 |
[WhiteheadRussell] p.
124 | Theorem *5.24 | pm5.24 934 |
[WhiteheadRussell] p.
124 | Theorem *5.25 | dfor2 426 |
[WhiteheadRussell] p.
125 | Theorem *5.3 | pm5.3 744 |
[WhiteheadRussell] p.
125 | Theorem *5.4 | pm5.4 376 |
[WhiteheadRussell] p.
125 | Theorem *5.5 | pm5.5 350 |
[WhiteheadRussell] p.
125 | Theorem *5.6 | pm5.6 949 |
[WhiteheadRussell] p.
125 | Theorem *5.7 | pm5.7 971 |
[WhiteheadRussell] p.
125 | Theorem *5.31 | pm5.31 610 |
[WhiteheadRussell] p.
125 | Theorem *5.32 | pm5.32 666 |
[WhiteheadRussell] p.
125 | Theorem *5.33 | pm5.33 918 |
[WhiteheadRussell] p.
125 | Theorem *5.35 | pm5.35 940 |
[WhiteheadRussell] p.
125 | Theorem *5.36 | pm5.36 919 |
[WhiteheadRussell] p.
125 | Theorem *5.41 | imdi 377 pm5.41 378 |
[WhiteheadRussell] p.
125 | Theorem *5.42 | pm5.42 569 |
[WhiteheadRussell] p.
125 | Theorem *5.44 | pm5.44 948 |
[WhiteheadRussell] p.
125 | Theorem *5.53 | pm5.53 833 |
[WhiteheadRussell] p.
125 | Theorem *5.54 | pm5.54 941 |
[WhiteheadRussell] p.
125 | Theorem *5.55 | pm5.55 937 |
[WhiteheadRussell] p.
125 | Theorem *5.61 | pm5.61 745 |
[WhiteheadRussell] p.
125 | Theorem *5.62 | pm5.62 960 |
[WhiteheadRussell] p.
125 | Theorem *5.63 | pm5.63 961 |
[WhiteheadRussell] p.
125 | Theorem *5.71 | pm5.71 973 |
[WhiteheadRussell] p.
125 | Theorem *5.501 | pm5.501 355 |
[WhiteheadRussell] p.
126 | Theorem *5.74 | pm5.74 258 |
[WhiteheadRussell] p.
126 | Theorem *5.75 | pm5.75 974 |
[WhiteheadRussell] p.
146 | Theorem *10.12 | pm10.12 37579 |
[WhiteheadRussell] p.
146 | Theorem *10.14 | pm10.14 37580 |
[WhiteheadRussell] p.
147 | Theorem *10.22 | 19.26 1786 |
[WhiteheadRussell] p.
149 | Theorem *10.251 | pm10.251 37581 |
[WhiteheadRussell] p.
149 | Theorem *10.252 | pm10.252 37582 |
[WhiteheadRussell] p.
149 | Theorem *10.253 | pm10.253 37583 |
[WhiteheadRussell] p.
150 | Theorem *10.3 | alsyl 1811 |
[WhiteheadRussell] p.
151 | Theorem *10.301 | albitr 37584 |
[WhiteheadRussell] p.
155 | Theorem *10.42 | pm10.42 37585 |
[WhiteheadRussell] p.
155 | Theorem *10.52 | pm10.52 37586 |
[WhiteheadRussell] p.
155 | Theorem *10.53 | pm10.53 37587 |
[WhiteheadRussell] p.
155 | Theorem *10.541 | pm10.541 37588 |
[WhiteheadRussell] p.
156 | Theorem *10.55 | pm10.55 37590 |
[WhiteheadRussell] p.
156 | Theorem *10.56 | pm10.56 37591 |
[WhiteheadRussell] p.
156 | Theorem *10.57 | pm10.57 37592 |
[WhiteheadRussell] p.
156 | Theorem *10.542 | pm10.542 37589 |
[WhiteheadRussell] p.
159 | Axiom *11.07 | pm11.07 2435 |
[WhiteheadRussell] p.
159 | Theorem *11.11 | pm11.11 37595 |
[WhiteheadRussell] p.
159 | Theorem *11.12 | pm11.12 37596 |
[WhiteheadRussell] p.
159 | Theorem PM*11.1 | 2stdpc4 2342 |
[WhiteheadRussell] p.
160 | Theorem *11.21 | alrot3 2025 |
[WhiteheadRussell] p.
160 | Theorem *11.22 | 2exnaln 1746 |
[WhiteheadRussell] p.
160 | Theorem *11.25 | 2nexaln 1747 |
[WhiteheadRussell] p.
161 | Theorem *11.3 | 19.21vv 37597 |
[WhiteheadRussell] p.
162 | Theorem *11.32 | 2alim 37598 |
[WhiteheadRussell] p.
162 | Theorem *11.33 | 2albi 37599 |
[WhiteheadRussell] p.
162 | Theorem *11.34 | 2exim 37600 |
[WhiteheadRussell] p.
162 | Theorem *11.36 | spsbce-2 37602 |
[WhiteheadRussell] p.
162 | Theorem *11.341 | 2exbi 37601 |
[WhiteheadRussell] p.
163 | Theorem *11.42 | 19.40-2 1803 |
[WhiteheadRussell] p.
163 | Theorem *11.43 | 19.36vv 37604 |
[WhiteheadRussell] p.
163 | Theorem *11.44 | 19.31vv 37605 |
[WhiteheadRussell] p.
163 | Theorem *11.421 | 19.33-2 37603 |
[WhiteheadRussell] p.
164 | Theorem *11.5 | 2nalexn 1745 |
[WhiteheadRussell] p.
164 | Theorem *11.46 | 19.37vv 37606 |
[WhiteheadRussell] p.
164 | Theorem *11.47 | 19.28vv 37607 |
[WhiteheadRussell] p.
164 | Theorem *11.51 | 2exnexn 1761 |
[WhiteheadRussell] p.
164 | Theorem *11.52 | pm11.52 37608 |
[WhiteheadRussell] p.
164 | Theorem *11.53 | pm11.53 2167 |
[WhiteheadRussell] p.
164 | Theorem *11.521 | 2exanali 37609 |
[WhiteheadRussell] p.
165 | Theorem *11.6 | pm11.6 37614 |
[WhiteheadRussell] p.
165 | Theorem *11.56 | aaanv 37610 |
[WhiteheadRussell] p.
165 | Theorem *11.57 | pm11.57 37611 |
[WhiteheadRussell] p.
165 | Theorem *11.58 | pm11.58 37612 |
[WhiteheadRussell] p.
165 | Theorem *11.59 | pm11.59 37613 |
[WhiteheadRussell] p.
166 | Theorem *11.7 | pm11.7 37618 |
[WhiteheadRussell] p.
166 | Theorem *11.61 | pm11.61 37615 |
[WhiteheadRussell] p.
166 | Theorem *11.62 | pm11.62 37616 |
[WhiteheadRussell] p.
166 | Theorem *11.63 | pm11.63 37617 |
[WhiteheadRussell] p.
166 | Theorem *11.71 | pm11.71 37619 |
[WhiteheadRussell] p.
175 | Definition *14.02 | df-eu 2462 |
[WhiteheadRussell] p.
178 | Theorem *13.13 | pm13.13a 37630 pm13.13b 37631 |
[WhiteheadRussell] p.
178 | Theorem *13.14 | pm13.14 37632 |
[WhiteheadRussell] p.
178 | Theorem *13.18 | pm13.18 2863 |
[WhiteheadRussell] p.
178 | Theorem *13.181 | pm13.181 2864 |
[WhiteheadRussell] p.
178 | Theorem *13.183 | pm13.183 3313 |
[WhiteheadRussell] p.
179 | Theorem *13.21 | 2sbc6g 37638 |
[WhiteheadRussell] p.
179 | Theorem *13.22 | 2sbc5g 37639 |
[WhiteheadRussell] p.
179 | Theorem *13.192 | pm13.192 37633 |
[WhiteheadRussell] p.
179 | Theorem *13.193 | 2pm13.193 37789 pm13.193 37634 |
[WhiteheadRussell] p.
179 | Theorem *13.194 | pm13.194 37635 |
[WhiteheadRussell] p.
179 | Theorem *13.195 | pm13.195 37636 |
[WhiteheadRussell] p.
179 | Theorem *13.196 | pm13.196a 37637 |
[WhiteheadRussell] p.
184 | Theorem *14.12 | pm14.12 37644 |
[WhiteheadRussell] p.
184 | Theorem *14.111 | iotasbc2 37643 |
[WhiteheadRussell] p.
184 | Definition *14.01 | iotasbc 37642 |
[WhiteheadRussell] p.
185 | Theorem *14.121 | sbeqalb 3455 |
[WhiteheadRussell] p.
185 | Theorem *14.122 | pm14.122a 37645 pm14.122b 37646 pm14.122c 37647 |
[WhiteheadRussell] p.
185 | Theorem *14.123 | pm14.123a 37648 pm14.123b 37649 pm14.123c 37650 |
[WhiteheadRussell] p.
189 | Theorem *14.2 | iotaequ 37652 |
[WhiteheadRussell] p.
189 | Theorem *14.18 | pm14.18 37651 |
[WhiteheadRussell] p.
189 | Theorem *14.202 | iotavalb 37653 |
[WhiteheadRussell] p.
190 | Theorem *14.22 | iota4 5786 |
[WhiteheadRussell] p.
190 | Theorem *14.205 | iotasbc5 37654 |
[WhiteheadRussell] p.
191 | Theorem *14.23 | iota4an 5787 |
[WhiteheadRussell] p.
191 | Theorem *14.24 | pm14.24 37655 |
[WhiteheadRussell] p.
192 | Theorem *14.25 | sbiota1 37657 |
[WhiteheadRussell] p.
192 | Theorem *14.26 | eupick 2524 eupickbi 2527 sbaniota 37658 |
[WhiteheadRussell] p.
192 | Theorem *14.242 | iotavalsb 37656 |
[WhiteheadRussell] p.
192 | Theorem *14.271 | eubi 37659 |
[WhiteheadRussell] p.
193 | Theorem *14.272 | iotasbcq 37660 |
[WhiteheadRussell] p.
235 | Definition *30.01 | conventions 26650 df-fv 5812 |
[WhiteheadRussell] p.
360 | Theorem *54.43 | pm54.43 8709 pm54.43lem 8708 |
[Young] p.
141 | Definition of operator ordering | leop2 28367 |
[Young] p.
142 | Example 12.2(i) | 0leop 28373 idleop 28374 |
[vandenDries] p. 42 | Lemma
61 | irrapx1 36410 |
[vandenDries] p. 43 | Theorem
62 | pellex 36417 pellexlem1 36411 |