Bibliographic Cross-Reference for the Metamath Proof Explorer
Bibliographic Reference | Description | Metamath Proof Explorer Page(s) |
[Adamek] p.
21 | Definition 3.1 | df-cat 16688 |
[Adamek] p. 21 | Condition
3.1(b) | df-cat 16688 |
[Adamek] p. 22 | Example
3.3(1) | df-setc 17085 |
[Adamek] p. 24 | Example
3.3(4.c) | 0cat 16708 |
[Adamek] p.
25 | Definition 3.5 | df-oppc 16731 |
[Adamek] p. 28 | Remark
3.9 | oppciso 16800 |
[Adamek] p. 28 | Remark
3.12 | invf1o 16788 invisoinvl 16809 |
[Adamek] p. 28 | Example
3.13 | idinv 16808 idiso 16807 |
[Adamek] p. 28 | Corollary
3.11 | inveq 16793 |
[Adamek] p.
28 | Definition 3.8 | df-inv 16767 df-iso 16768 dfiso2 16791 |
[Adamek] p.
28 | Proposition 3.10 | sectcan 16774 |
[Adamek] p. 29 | Remark
3.16 | cicer 16825 |
[Adamek] p.
29 | Definition 3.15 | cic 16818 df-cic 16815 |
[Adamek] p.
29 | Definition 3.17 | df-func 16877 |
[Adamek] p.
29 | Proposition 3.14(1) | invinv 16789 |
[Adamek] p.
29 | Proposition 3.14(2) | invco 16790 isoco 16796 |
[Adamek] p. 30 | Remark
3.19 | df-func 16877 |
[Adamek] p. 30 | Example
3.20(1) | idfucl 16900 |
[Adamek] p.
32 | Proposition 3.21 | funciso 16893 |
[Adamek] p.
33 | Proposition 3.23 | cofucl 16907 |
[Adamek] p. 34 | Remark
3.28(2) | catciso 17116 |
[Adamek] p. 34 | Remark
3.28 (1) | embedsetcestrc 17167 |
[Adamek] p.
34 | Definition 3.27(2) | df-fth 16924 |
[Adamek] p.
34 | Definition 3.27(3) | df-full 16923 |
[Adamek] p.
34 | Definition 3.27 (1) | embedsetcestrc 17167 |
[Adamek] p. 35 | Corollary
3.32 | ffthiso 16948 |
[Adamek] p.
35 | Proposition 3.30(c) | cofth 16954 |
[Adamek] p.
35 | Proposition 3.30(d) | cofull 16953 |
[Adamek] p.
36 | Definition 3.33 (1) | equivestrcsetc 17152 |
[Adamek] p.
36 | Definition 3.33 (2) | equivestrcsetc 17152 |
[Adamek] p.
39 | Definition 3.41 | funcoppc 16894 |
[Adamek] p.
39 | Definition 3.44. | df-catc 17104 |
[Adamek] p.
39 | Proposition 3.43(c) | fthoppc 16942 |
[Adamek] p.
39 | Proposition 3.43(d) | fulloppc 16941 |
[Adamek] p. 40 | Remark
3.48 | catccat 17113 |
[Adamek] p.
40 | Definition 3.47 | df-catc 17104 |
[Adamek] p. 48 | Example
4.3(1.a) | 0subcat 16857 |
[Adamek] p. 48 | Example
4.3(1.b) | catsubcat 16858 |
[Adamek] p.
48 | Definition 4.1(2) | fullsubc 16869 |
[Adamek] p.
48 | Definition 4.1(a) | df-subc 16831 |
[Adamek] p. 49 | Remark
4.4(2) | ressffth 16957 |
[Adamek] p.
83 | Definition 6.1 | df-nat 16962 |
[Adamek] p. 87 | Remark
6.14(a) | fuccocl 16983 |
[Adamek] p. 87 | Remark
6.14(b) | fucass 16987 |
[Adamek] p.
87 | Definition 6.15 | df-fuc 16963 |
[Adamek] p. 88 | Remark
6.16 | fuccat 16989 |
[Adamek] p.
101 | Definition 7.1 | df-inito 17000 |
[Adamek] p.
101 | Example 7.2 (6) | irinitoringc 42930 |
[Adamek] p.
102 | Definition 7.4 | df-termo 17001 |
[Adamek] p.
102 | Proposition 7.3 (1) | initoeu1w 17021 |
[Adamek] p.
102 | Proposition 7.3 (2) | initoeu2 17025 |
[Adamek] p.
103 | Definition 7.7 | df-zeroo 17002 |
[Adamek] p.
103 | Example 7.9 (3) | nzerooringczr 42933 |
[Adamek] p.
103 | Proposition 7.6 | termoeu1w 17028 |
[Adamek] p.
106 | Definition 7.19 | df-sect 16766 |
[Adamek] p.
478 | Item Rng | df-ringc 42866 |
[AhoHopUll]
p. 2 | Section 1.1 | df-bigo 43203 |
[AhoHopUll]
p. 12 | Section 1.3 | df-blen 43225 |
[AhoHopUll] p.
318 | Section 9.1 | df-concat 13638 df-pfx 13757 df-substr 13708 df-word 13582 lencl 13600 wrd0 13606 |
[AkhiezerGlazman] p.
39 | Linear operator norm | df-nmo 22889 df-nmoo 28151 |
[AkhiezerGlazman] p.
64 | Theorem | hmopidmch 29563 hmopidmchi 29561 |
[AkhiezerGlazman] p. 65 | Theorem
1 | pjcmul1i 29611 pjcmul2i 29612 |
[AkhiezerGlazman] p.
72 | Theorem | cnvunop 29328 unoplin 29330 |
[AkhiezerGlazman] p. 72 | Equation
2 | unopadj 29329 unopadj2 29348 |
[AkhiezerGlazman] p.
73 | Theorem | elunop2 29423 lnopunii 29422 |
[AkhiezerGlazman] p.
80 | Proposition 1 | adjlnop 29496 |
[Apostol] p. 18 | Theorem
I.1 | addcan 10546 addcan2d 10566 addcan2i 10556 addcand 10565 addcani 10555 |
[Apostol] p. 18 | Theorem
I.2 | negeu 10598 |
[Apostol] p. 18 | Theorem
I.3 | negsub 10657 negsubd 10726 negsubi 10687 |
[Apostol] p. 18 | Theorem
I.4 | negneg 10659 negnegd 10711 negnegi 10679 |
[Apostol] p. 18 | Theorem
I.5 | subdi 10794 subdid 10817 subdii 10810 subdir 10795 subdird 10818 subdiri 10811 |
[Apostol] p. 18 | Theorem
I.6 | mul01 10541 mul01d 10561 mul01i 10552 mul02 10540 mul02d 10560 mul02i 10551 |
[Apostol] p. 18 | Theorem
I.7 | mulcan 10996 mulcan2d 10993 mulcand 10992 mulcani 10998 |
[Apostol] p. 18 | Theorem
I.8 | receu 11004 xreceu 30171 |
[Apostol] p. 18 | Theorem
I.9 | divrec 11033 divrecd 11137 divreci 11103 divreczi 11096 |
[Apostol] p. 18 | Theorem
I.10 | recrec 11055 recreci 11090 |
[Apostol] p. 18 | Theorem
I.11 | mul0or 10999 mul0ord 11009 mul0ori 11007 |
[Apostol] p. 18 | Theorem
I.12 | mul2neg 10800 mul2negd 10816 mul2negi 10809 mulneg1 10797 mulneg1d 10814 mulneg1i 10807 |
[Apostol] p. 18 | Theorem
I.13 | divadddiv 11073 divadddivd 11178 divadddivi 11120 |
[Apostol] p. 18 | Theorem
I.14 | divmuldiv 11058 divmuldivd 11175 divmuldivi 11118 rdivmuldivd 30332 |
[Apostol] p. 18 | Theorem
I.15 | divdivdiv 11059 divdivdivd 11181 divdivdivi 11121 |
[Apostol] p. 20 | Axiom
7 | rpaddcl 12143 rpaddcld 12178 rpmulcl 12144 rpmulcld 12179 |
[Apostol] p. 20 | Axiom
8 | rpneg 12153 |
[Apostol] p. 20 | Axiom
9 | 0nrp 12156 |
[Apostol] p. 20 | Theorem
I.17 | lttri 10489 |
[Apostol] p. 20 | Theorem
I.18 | ltadd1d 10952 ltadd1dd 10970 ltadd1i 10913 |
[Apostol] p. 20 | Theorem
I.19 | ltmul1 11210 ltmul1a 11209 ltmul1i 11279 ltmul1ii 11289 ltmul2 11211 ltmul2d 12205 ltmul2dd 12219 ltmul2i 11282 |
[Apostol] p. 20 | Theorem
I.20 | msqgt0 10879 msqgt0d 10926 msqgt0i 10896 |
[Apostol] p. 20 | Theorem
I.21 | 0lt1 10881 |
[Apostol] p. 20 | Theorem
I.23 | lt0neg1 10865 lt0neg1d 10928 ltneg 10859 ltnegd 10937 ltnegi 10903 |
[Apostol] p. 20 | Theorem
I.25 | lt2add 10844 lt2addd 10982 lt2addi 10921 |
[Apostol] p.
20 | Definition of positive numbers | df-rp 12120 |
[Apostol] p.
21 | Exercise 4 | recgt0 11204 recgt0d 11295 recgt0i 11265 recgt0ii 11266 |
[Apostol] p.
22 | Definition of integers | df-z 11712 |
[Apostol] p.
22 | Definition of positive integers | dfnn3 11373 |
[Apostol] p.
22 | Definition of rationals | df-q 12079 |
[Apostol] p. 24 | Theorem
I.26 | supeu 8635 |
[Apostol] p. 26 | Theorem
I.28 | nnunb 11621 |
[Apostol] p. 26 | Theorem
I.29 | arch 11622 |
[Apostol] p.
28 | Exercise 2 | btwnz 11814 |
[Apostol] p.
28 | Exercise 3 | nnrecl 11623 |
[Apostol] p.
28 | Exercise 4 | rebtwnz 12077 |
[Apostol] p.
28 | Exercise 5 | zbtwnre 12076 |
[Apostol] p.
28 | Exercise 6 | qbtwnre 12325 |
[Apostol] p.
28 | Exercise 10(a) | zeneo 15444 zneo 11795 zneoALTV 42424 |
[Apostol] p. 29 | Theorem
I.35 | cxpsqrtth 24881 msqsqrtd 14563 resqrtth 14380 sqrtth 14488 sqrtthi 14494 sqsqrtd 14562 |
[Apostol] p. 34 | Theorem
I.36 (principle of mathematical induction) | peano5nni 11360 |
[Apostol] p. 34 | Theorem
I.37 (well-ordering principle) | nnwo 12043 |
[Apostol] p.
361 | Remark | crreczi 13290 |
[Apostol] p.
363 | Remark | absgt0i 14522 |
[Apostol] p.
363 | Example | abssubd 14576 abssubi 14526 |
[ApostolNT]
p. 7 | Remark | fmtno0 42296 fmtno1 42297 fmtno2 42306 fmtno3 42307 fmtno4 42308 fmtno5fac 42338 fmtnofz04prm 42333 |
[ApostolNT]
p. 7 | Definition | df-fmtno 42284 |
[ApostolNT] p.
8 | Definition | df-ppi 25246 |
[ApostolNT] p.
14 | Definition | df-dvds 15365 |
[ApostolNT] p.
14 | Theorem 1.1(a) | iddvds 15379 |
[ApostolNT] p.
14 | Theorem 1.1(b) | dvdstr 15402 |
[ApostolNT] p.
14 | Theorem 1.1(c) | dvds2ln 15398 |
[ApostolNT] p.
14 | Theorem 1.1(d) | dvdscmul 15392 |
[ApostolNT] p.
14 | Theorem 1.1(e) | dvdscmulr 15394 |
[ApostolNT] p.
14 | Theorem 1.1(f) | 1dvds 15380 |
[ApostolNT] p.
14 | Theorem 1.1(g) | dvds0 15381 |
[ApostolNT] p.
14 | Theorem 1.1(h) | 0dvds 15386 |
[ApostolNT] p.
14 | Theorem 1.1(i) | dvdsleabs 15417 |
[ApostolNT] p.
14 | Theorem 1.1(j) | dvdsabseq 15419 |
[ApostolNT] p.
14 | Theorem 1.1(k) | divconjdvds 15421 |
[ApostolNT] p.
15 | Definition | df-gcd 15597 dfgcd2 15643 |
[ApostolNT] p.
16 | Definition | isprm2 15774 |
[ApostolNT] p.
16 | Theorem 1.5 | coprmdvds 15746 |
[ApostolNT] p.
16 | Theorem 1.7 | prminf 15997 |
[ApostolNT] p.
16 | Theorem 1.4(a) | gcdcom 15615 |
[ApostolNT] p.
16 | Theorem 1.4(b) | gcdass 15644 |
[ApostolNT] p.
16 | Theorem 1.4(c) | absmulgcd 15646 |
[ApostolNT] p.
16 | Theorem 1.4(d)1 | gcd1 15629 |
[ApostolNT] p.
16 | Theorem 1.4(d)2 | gcdid0 15621 |
[ApostolNT] p.
17 | Theorem 1.8 | coprm 15801 |
[ApostolNT] p.
17 | Theorem 1.9 | euclemma 15803 |
[ApostolNT] p.
17 | Theorem 1.10 | 1arith2 16010 |
[ApostolNT] p.
18 | Theorem 1.13 | prmrec 16004 |
[ApostolNT] p.
19 | Theorem 1.14 | divalg 15507 |
[ApostolNT] p.
20 | Theorem 1.15 | eucalg 15680 |
[ApostolNT] p.
24 | Definition | df-mu 25247 |
[ApostolNT] p.
25 | Definition | df-phi 15849 |
[ApostolNT] p.
25 | Theorem 2.1 | musum 25337 |
[ApostolNT] p.
26 | Theorem 2.2 | phisum 15873 |
[ApostolNT] p.
28 | Theorem 2.5(a) | phiprmpw 15859 |
[ApostolNT] p.
28 | Theorem 2.5(c) | phimul 15863 |
[ApostolNT] p.
32 | Definition | df-vma 25244 |
[ApostolNT] p.
32 | Theorem 2.9 | muinv 25339 |
[ApostolNT] p.
32 | Theorem 2.10 | vmasum 25361 |
[ApostolNT] p.
38 | Remark | df-sgm 25248 |
[ApostolNT] p.
38 | Definition | df-sgm 25248 |
[ApostolNT] p.
75 | Definition | df-chp 25245 df-cht 25243 |
[ApostolNT] p.
104 | Definition | congr 15757 |
[ApostolNT] p.
106 | Remark | dvdsval3 15368 |
[ApostolNT] p.
106 | Definition | moddvds 15375 |
[ApostolNT] p.
107 | Example 2 | mod2eq0even 15451 |
[ApostolNT] p.
107 | Example 3 | mod2eq1n2dvds 15452 |
[ApostolNT] p.
107 | Example 4 | zmod1congr 12989 |
[ApostolNT] p.
107 | Theorem 5.2(b) | modmul12d 13026 |
[ApostolNT] p.
107 | Theorem 5.2(c) | modexp 13300 |
[ApostolNT] p.
108 | Theorem 5.3 | modmulconst 15397 |
[ApostolNT] p.
109 | Theorem 5.4 | cncongr1 15760 |
[ApostolNT] p.
109 | Theorem 5.6 | gcdmodi 16156 |
[ApostolNT] p.
109 | Theorem 5.4 "Cancellation law" | cncongr 15762 |
[ApostolNT] p.
113 | Theorem 5.17 | eulerth 15866 |
[ApostolNT] p.
113 | Theorem 5.18 | vfermltl 15884 |
[ApostolNT] p.
114 | Theorem 5.19 | fermltl 15867 |
[ApostolNT] p.
116 | Theorem 5.24 | wilthimp 25218 |
[ApostolNT] p.
179 | Definition | df-lgs 25440 lgsprme0 25484 |
[ApostolNT] p.
180 | Example 1 | 1lgs 25485 |
[ApostolNT] p.
180 | Theorem 9.2 | lgsvalmod 25461 |
[ApostolNT] p.
180 | Theorem 9.3 | lgsdirprm 25476 |
[ApostolNT] p.
181 | Theorem 9.4 | m1lgs 25533 |
[ApostolNT] p.
181 | Theorem 9.5 | 2lgs 25552 2lgsoddprm 25561 |
[ApostolNT] p.
182 | Theorem 9.6 | gausslemma2d 25519 |
[ApostolNT] p.
185 | Theorem 9.8 | lgsquad 25528 |
[ApostolNT] p.
188 | Definition | df-lgs 25440 lgs1 25486 |
[ApostolNT] p.
188 | Theorem 9.9(a) | lgsdir 25477 |
[ApostolNT] p.
188 | Theorem 9.9(b) | lgsdi 25479 |
[ApostolNT] p.
188 | Theorem 9.9(c) | lgsmodeq 25487 |
[ApostolNT] p.
188 | Theorem 9.9(d) | lgsmulsqcoprm 25488 |
[Baer] p.
40 | Property (b) | mapdord 37708 |
[Baer] p.
40 | Property (c) | mapd11 37709 |
[Baer] p.
40 | Property (e) | mapdin 37732 mapdlsm 37734 |
[Baer] p.
40 | Property (f) | mapd0 37735 |
[Baer] p.
40 | Definition of projectivity | df-mapd 37695 mapd1o 37718 |
[Baer] p.
41 | Property (g) | mapdat 37737 |
[Baer] p.
44 | Part (1) | mapdpg 37776 |
[Baer] p.
45 | Part (2) | hdmap1eq 37871 mapdheq 37798 mapdheq2 37799 mapdheq2biN 37800 |
[Baer] p.
45 | Part (3) | baerlem3 37783 |
[Baer] p.
46 | Part (4) | mapdheq4 37802 mapdheq4lem 37801 |
[Baer] p.
46 | Part (5) | baerlem5a 37784 baerlem5abmN 37788 baerlem5amN 37786 baerlem5b 37785 baerlem5bmN 37787 |
[Baer] p.
47 | Part (6) | hdmap1l6 37891 hdmap1l6a 37879 hdmap1l6e 37884 hdmap1l6f 37885 hdmap1l6g 37886 hdmap1l6lem1 37877 hdmap1l6lem2 37878 mapdh6N 37817 mapdh6aN 37805 mapdh6eN 37810 mapdh6fN 37811 mapdh6gN 37812 mapdh6lem1N 37803 mapdh6lem2N 37804 |
[Baer] p.
48 | Part 9 | hdmapval 37898 |
[Baer] p.
48 | Part 10 | hdmap10 37910 |
[Baer] p.
48 | Part 11 | hdmapadd 37913 |
[Baer] p.
48 | Part (6) | hdmap1l6h 37887 mapdh6hN 37813 |
[Baer] p.
48 | Part (7) | mapdh75cN 37823 mapdh75d 37824 mapdh75e 37822 mapdh75fN 37825 mapdh7cN 37819 mapdh7dN 37820 mapdh7eN 37818 mapdh7fN 37821 |
[Baer] p.
48 | Part (8) | mapdh8 37858 mapdh8a 37845 mapdh8aa 37846 mapdh8ab 37847 mapdh8ac 37848 mapdh8ad 37849 mapdh8b 37850 mapdh8c 37851 mapdh8d 37853 mapdh8d0N 37852 mapdh8e 37854 mapdh8g 37855 mapdh8i 37856 mapdh8j 37857 |
[Baer] p.
48 | Part (9) | mapdh9a 37859 |
[Baer] p.
48 | Equation 10 | mapdhvmap 37839 |
[Baer] p.
49 | Part 12 | hdmap11 37918 hdmapeq0 37914 hdmapf1oN 37935 hdmapneg 37916 hdmaprnN 37934 hdmaprnlem1N 37919 hdmaprnlem3N 37920 hdmaprnlem3uN 37921 hdmaprnlem4N 37923 hdmaprnlem6N 37924 hdmaprnlem7N 37925 hdmaprnlem8N 37926 hdmaprnlem9N 37927 hdmapsub 37917 |
[Baer] p.
49 | Part 14 | hdmap14lem1 37938 hdmap14lem10 37947 hdmap14lem1a 37936 hdmap14lem2N 37939 hdmap14lem2a 37937 hdmap14lem3 37940 hdmap14lem8 37945 hdmap14lem9 37946 |
[Baer] p.
50 | Part 14 | hdmap14lem11 37948 hdmap14lem12 37949 hdmap14lem13 37950 hdmap14lem14 37951 hdmap14lem15 37952 hgmapval 37957 |
[Baer] p.
50 | Part 15 | hgmapadd 37964 hgmapmul 37965 hgmaprnlem2N 37967 hgmapvs 37961 |
[Baer] p.
50 | Part 16 | hgmaprnN 37971 |
[Baer] p.
110 | Lemma 1 | hdmapip0com 37987 |
[Baer] p.
110 | Line 27 | hdmapinvlem1 37988 |
[Baer] p.
110 | Line 28 | hdmapinvlem2 37989 |
[Baer] p.
110 | Line 30 | hdmapinvlem3 37990 |
[Baer] p.
110 | Part 1.2 | hdmapglem5 37992 hgmapvv 37996 |
[Baer] p.
110 | Proposition 1 | hdmapinvlem4 37991 |
[Baer] p.
111 | Line 10 | hgmapvvlem1 37993 |
[Baer] p.
111 | Line 15 | hdmapg 38000 hdmapglem7 37999 |
[Bauer], p. 483 | Theorem
1.2 | 2irrexpq 24882 2irrexpqALT 24947 |
[BellMachover] p.
36 | Lemma 10.3 | idALT 23 |
[BellMachover] p.
97 | Definition 10.1 | df-eu 2640 |
[BellMachover] p.
460 | Notation | df-mo 2605 |
[BellMachover] p.
460 | Definition | mo3 2633 |
[BellMachover] p.
461 | Axiom Ext | ax-ext 2803 |
[BellMachover] p.
462 | Theorem 1.1 | axextmo 2808 |
[BellMachover] p.
463 | Axiom Rep | axrep5 5002 |
[BellMachover] p.
463 | Scheme Sep | axsep 5006 |
[BellMachover] p. 463 | Theorem
1.3(ii) | bj-bm1.3ii 33541 bm1.3ii 5010 |
[BellMachover] p.
466 | Problem | axpow2 5069 |
[BellMachover] p.
466 | Axiom Pow | axpow3 5070 |
[BellMachover] p.
466 | Axiom Union | axun2 7216 |
[BellMachover] p.
468 | Definition | df-ord 5970 |
[BellMachover] p.
469 | Theorem 2.2(i) | ordirr 5985 |
[BellMachover] p.
469 | Theorem 2.2(iii) | onelon 5992 |
[BellMachover] p.
469 | Theorem 2.2(vii) | ordn2lp 5987 |
[BellMachover] p.
471 | Definition of N | df-om 7332 |
[BellMachover] p.
471 | Problem 2.5(ii) | uniordint 7272 |
[BellMachover] p.
471 | Definition of Lim | df-lim 5972 |
[BellMachover] p.
472 | Axiom Inf | zfinf2 8823 |
[BellMachover] p.
473 | Theorem 2.8 | limom 7346 |
[BellMachover] p.
477 | Equation 3.1 | df-r1 8911 |
[BellMachover] p.
478 | Definition | rankval2 8965 |
[BellMachover] p.
478 | Theorem 3.3(i) | r1ord3 8929 r1ord3g 8926 |
[BellMachover] p.
480 | Axiom Reg | zfreg 8776 |
[BellMachover] p.
488 | Axiom AC | ac5 9621 dfac4 9265 |
[BellMachover] p.
490 | Definition of aleph | alephval3 9253 |
[BeltramettiCassinelli] p.
98 | Remark | atlatmstc 35389 |
[BeltramettiCassinelli] p.
107 | Remark 10.3.5 | atom1d 29763 |
[BeltramettiCassinelli] p.
166 | Theorem 14.8.4 | chirred 29805 chirredi 29804 |
[BeltramettiCassinelli1] p.
400 | Proposition P8(ii) | atoml2i 29793 |
[Beran] p.
3 | Definition of join | sshjval3 28764 |
[Beran] p.
39 | Theorem 2.3(i) | cmcm2 29026 cmcm2i 29003 cmcm2ii 29008 cmt2N 35320 |
[Beran] p.
40 | Theorem 2.3(iii) | lecm 29027 lecmi 29012 lecmii 29013 |
[Beran] p.
45 | Theorem 3.4 | cmcmlem 29001 |
[Beran] p.
49 | Theorem 4.2 | cm2j 29030 cm2ji 29035 cm2mi 29036 |
[Beran] p.
95 | Definition | df-sh 28615 issh2 28617 |
[Beran] p.
95 | Lemma 3.1(S5) | his5 28494 |
[Beran] p.
95 | Lemma 3.1(S6) | his6 28507 |
[Beran] p.
95 | Lemma 3.1(S7) | his7 28498 |
[Beran] p.
95 | Lemma 3.2(S8) | ho01i 29238 |
[Beran] p.
95 | Lemma 3.2(S9) | hoeq1 29240 |
[Beran] p.
95 | Lemma 3.2(S10) | ho02i 29239 |
[Beran] p.
95 | Lemma 3.2(S11) | hoeq2 29241 |
[Beran] p.
95 | Postulate (S1) | ax-his1 28490 his1i 28508 |
[Beran] p.
95 | Postulate (S2) | ax-his2 28491 |
[Beran] p.
95 | Postulate (S3) | ax-his3 28492 |
[Beran] p.
95 | Postulate (S4) | ax-his4 28493 |
[Beran] p.
96 | Definition of norm | df-hnorm 28376 dfhnorm2 28530 normval 28532 |
[Beran] p.
96 | Definition for Cauchy sequence | hcau 28592 |
[Beran] p.
96 | Definition of Cauchy sequence | df-hcau 28381 |
[Beran] p.
96 | Definition of complete subspace | isch3 28649 |
[Beran] p.
96 | Definition of converge | df-hlim 28380 hlimi 28596 |
[Beran] p.
97 | Theorem 3.3(i) | norm-i-i 28541 norm-i 28537 |
[Beran] p.
97 | Theorem 3.3(ii) | norm-ii-i 28545 norm-ii 28546 normlem0 28517 normlem1 28518 normlem2 28519 normlem3 28520 normlem4 28521 normlem5 28522 normlem6 28523 normlem7 28524 normlem7tALT 28527 |
[Beran] p.
97 | Theorem 3.3(iii) | norm-iii-i 28547 norm-iii 28548 |
[Beran] p.
98 | Remark 3.4 | bcs 28589 bcsiALT 28587 bcsiHIL 28588 |
[Beran] p.
98 | Remark 3.4(B) | normlem9at 28529 normpar 28563 normpari 28562 |
[Beran] p.
98 | Remark 3.4(C) | normpyc 28554 normpyth 28553 normpythi 28550 |
[Beran] p.
99 | Remark | lnfn0 29457 lnfn0i 29452 lnop0 29376 lnop0i 29380 |
[Beran] p.
99 | Theorem 3.5(i) | nmcexi 29436 nmcfnex 29463 nmcfnexi 29461 nmcopex 29439 nmcopexi 29437 |
[Beran] p.
99 | Theorem 3.5(ii) | nmcfnlb 29464 nmcfnlbi 29462 nmcoplb 29440 nmcoplbi 29438 |
[Beran] p.
99 | Theorem 3.5(iii) | lnfncon 29466 lnfnconi 29465 lnopcon 29445 lnopconi 29444 |
[Beran] p.
100 | Lemma 3.6 | normpar2i 28564 |
[Beran] p.
101 | Lemma 3.6 | norm3adifi 28561 norm3adifii 28556 norm3dif 28558 norm3difi 28555 |
[Beran] p.
102 | Theorem 3.7(i) | chocunii 28711 pjhth 28803 pjhtheu 28804 pjpjhth 28835 pjpjhthi 28836 pjth 23614 |
[Beran] p.
102 | Theorem 3.7(ii) | ococ 28816 ococi 28815 |
[Beran] p.
103 | Remark 3.8 | nlelchi 29471 |
[Beran] p.
104 | Theorem 3.9 | riesz3i 29472 riesz4 29474 riesz4i 29473 |
[Beran] p.
104 | Theorem 3.10 | cnlnadj 29489 cnlnadjeu 29488 cnlnadjeui 29487 cnlnadji 29486 cnlnadjlem1 29477 nmopadjlei 29498 |
[Beran] p.
106 | Theorem 3.11(i) | adjeq0 29501 |
[Beran] p.
106 | Theorem 3.11(v) | nmopadji 29500 |
[Beran] p.
106 | Theorem 3.11(ii) | adjmul 29502 |
[Beran] p.
106 | Theorem 3.11(iv) | adjadj 29346 |
[Beran] p.
106 | Theorem 3.11(vi) | nmopcoadj2i 29512 nmopcoadji 29511 |
[Beran] p.
106 | Theorem 3.11(iii) | adjadd 29503 |
[Beran] p.
106 | Theorem 3.11(vii) | nmopcoadj0i 29513 |
[Beran] p.
106 | Theorem 3.11(viii) | adjcoi 29510 pjadj2coi 29614 pjadjcoi 29571 |
[Beran] p.
107 | Definition | df-ch 28629 isch2 28631 |
[Beran] p.
107 | Remark 3.12 | choccl 28716 isch3 28649 occl 28714 ocsh 28693 shoccl 28715 shocsh 28694 |
[Beran] p.
107 | Remark 3.12(B) | ococin 28818 |
[Beran] p.
108 | Theorem 3.13 | chintcl 28742 |
[Beran] p.
109 | Property (i) | pjadj2 29597 pjadj3 29598 pjadji 29095 pjadjii 29084 |
[Beran] p.
109 | Property (ii) | pjidmco 29591 pjidmcoi 29587 pjidmi 29083 |
[Beran] p.
110 | Definition of projector ordering | pjordi 29583 |
[Beran] p.
111 | Remark | ho0val 29160 pjch1 29080 |
[Beran] p.
111 | Definition | df-hfmul 29144 df-hfsum 29143 df-hodif 29142 df-homul 29141 df-hosum 29140 |
[Beran] p.
111 | Lemma 4.4(i) | pjo 29081 |
[Beran] p.
111 | Lemma 4.4(ii) | pjch 29104 pjchi 28842 |
[Beran] p.
111 | Lemma 4.4(iii) | pjoc2 28849 pjoc2i 28848 |
[Beran] p.
112 | Theorem 4.5(i)->(ii) | pjss2i 29090 |
[Beran] p.
112 | Theorem 4.5(i)->(iv) | pjssmi 29575 pjssmii 29091 |
[Beran] p.
112 | Theorem 4.5(i)<->(ii) | pjss2coi 29574 |
[Beran] p.
112 | Theorem 4.5(i)<->(iii) | pjss1coi 29573 |
[Beran] p.
112 | Theorem 4.5(i)<->(vi) | pjnormssi 29578 |
[Beran] p.
112 | Theorem 4.5(iv)->(v) | pjssge0i 29576 pjssge0ii 29092 |
[Beran] p.
112 | Theorem 4.5(v)<->(vi) | pjdifnormi 29577 pjdifnormii 29093 |
[Bobzien] p.
116 | Statement T3 | stoic3 1875 |
[Bobzien] p.
117 | Statement T2 | stoic2a 1873 |
[Bobzien] p.
117 | Statement T4 | stoic4a 1876 |
[Bobzien] p.
117 | Conclusion the contradictory | stoic1a 1871 |
[Bogachev]
p. 16 | Definition 1.5 | df-oms 30895 |
[Bogachev]
p. 17 | Lemma 1.5.4 | omssubadd 30903 |
[Bogachev]
p. 17 | Example 1.5.2 | omsmon 30901 |
[Bogachev]
p. 41 | Definition 1.11.2 | df-carsg 30905 |
[Bogachev]
p. 42 | Theorem 1.11.4 | carsgsiga 30925 |
[Bogachev]
p. 116 | Definition 2.3.1 | df-itgm 30956 df-sitm 30934 |
[Bogachev]
p. 118 | Chapter 2.4.4 | df-itgm 30956 |
[Bogachev]
p. 118 | Definition 2.4.1 | df-sitg 30933 |
[Bollobas] p.
1 | Section I.1 | df-edg 26353 isuhgrop 26375 isusgrop 26468 isuspgrop 26467 |
[Bollobas] p.
2 | Section I.1 | df-subgr 26572 uhgrspan1 26607 uhgrspansubgr 26595 |
[Bollobas]
p. 3 | Definition | isomuspgr 42566 |
[Bollobas] p.
3 | Section I.1 | cusgrsize 26759 df-cusgr 26717 df-nbgr 26637 fusgrmaxsize 26769 |
[Bollobas]
p. 4 | Definition | df-upwlks 42576 df-wlks 26904 |
[Bollobas] p.
4 | Section I.1 | finsumvtxdg2size 26855 finsumvtxdgeven 26857 fusgr1th 26856 fusgrvtxdgonume 26859 vtxdgoddnumeven 26858 |
[Bollobas] p.
5 | Notation | df-pths 27025 |
[Bollobas] p.
5 | Definition | df-crcts 27095 df-cycls 27096 df-trls 27000 df-wlkson 26905 |
[Bollobas] p.
7 | Section I.1 | df-ushgr 26364 |
[BourbakiAlg1] p. 1 | Definition
1 | df-clintop 42697 df-cllaw 42683 df-mgm 17602 df-mgm2 42716 |
[BourbakiAlg1] p. 4 | Definition
5 | df-assintop 42698 df-asslaw 42685 df-sgrp 17644 df-sgrp2 42718 |
[BourbakiAlg1] p. 7 | Definition
8 | df-cmgm2 42717 df-comlaw 42684 |
[BourbakiAlg1] p.
12 | Definition 2 | df-mnd 17655 |
[BourbakiAlg1] p.
92 | Definition 1 | df-ring 18910 |
[BourbakiAlg1] p. 93 | Section
I.8.1 | df-rng0 42736 |
[BourbakiEns] p.
| Proposition 8 | fcof1 6802 fcofo 6803 |
[BourbakiTop1] p.
| Remark | xnegmnf 12336 xnegpnf 12335 |
[BourbakiTop1] p.
| Remark | rexneg 12337 |
[BourbakiTop1] p.
| Remark 3 | ust0 22400 ustfilxp 22393 |
[BourbakiTop1] p.
| Axiom GT' | tgpsubcn 22271 |
[BourbakiTop1] p.
| Example 1 | cstucnd 22465 iducn 22464 snfil 22045 |
[BourbakiTop1] p.
| Example 2 | neifil 22061 |
[BourbakiTop1] p.
| Theorem 1 | cnextcn 22248 |
[BourbakiTop1] p.
| Theorem 2 | ucnextcn 22485 |
[BourbakiTop1] p. | Theorem
3 | df-hcmp 30544 |
[BourbakiTop1] p.
| Paragraph 3 | infil 22044 |
[BourbakiTop1] p.
| Proposition | ishmeo 21940 |
[BourbakiTop1] p.
| Definition 1 | df-ucn 22457 df-ust 22381 filintn0 22042 filn0 22043 istgp 22258 ucnprima 22463 |
[BourbakiTop1] p.
| Definition 2 | df-cfilu 22468 |
[BourbakiTop1] p.
| Definition 3 | df-cusp 22479 df-usp 22438 df-utop 22412 trust 22410 |
[BourbakiTop1] p. | Definition
6 | df-pcmp 30464 |
[BourbakiTop1] p.
| Property V_i | ssnei2 21298 |
[BourbakiTop1] p.
| Theorem 1(d) | iscncl 21451 |
[BourbakiTop1] p.
| Condition F_I | ustssel 22386 |
[BourbakiTop1] p.
| Condition U_I | ustdiag 22389 |
[BourbakiTop1] p.
| Property V_ii | innei 21307 |
[BourbakiTop1] p.
| Property V_iv | neiptopreu 21315 neissex 21309 |
[BourbakiTop1] p.
| Proposition 1 | neips 21295 neiss 21291 ucncn 22466 ustund 22402 ustuqtop 22427 |
[BourbakiTop1] p.
| Proposition 2 | cnpco 21449 neiptopreu 21315 utop2nei 22431 utop3cls 22432 |
[BourbakiTop1] p.
| Proposition 3 | fmucnd 22473 uspreg 22455 utopreg 22433 |
[BourbakiTop1] p.
| Proposition 4 | imasncld 21872 imasncls 21873 imasnopn 21871 |
[BourbakiTop1] p.
| Proposition 9 | cnpflf2 22181 |
[BourbakiTop1] p.
| Condition F_II | ustincl 22388 |
[BourbakiTop1] p.
| Condition U_II | ustinvel 22390 |
[BourbakiTop1] p.
| Property V_iii | elnei 21293 |
[BourbakiTop1] p.
| Proposition 11 | cnextucn 22484 |
[BourbakiTop1] p.
| Condition F_IIb | ustbasel 22387 |
[BourbakiTop1] p.
| Condition U_III | ustexhalf 22391 |
[BourbakiTop1] p.
| Definition C''' | df-cmp 21568 |
[BourbakiTop1] p.
| Axioms FI, FIIa, FIIb, FIII) | df-fil 22027 |
[BourbakiTop1] p.
| Definition is due to Bourbaki (Def. 1 | df-top 21076 |
[BourbakiTop2] p. 195 | Definition
1 | df-ldlf 30461 |
[BrosowskiDeutsh] p. 89 | Proof
follows | stoweidlem62 41067 |
[BrosowskiDeutsh] p. 89 | Lemmas
are written following | stowei 41069 stoweid 41068 |
[BrosowskiDeutsh] p. 90 | Lemma
1 | stoweidlem1 41006 stoweidlem10 41015 stoweidlem14 41019 stoweidlem15 41020 stoweidlem35 41040 stoweidlem36 41041 stoweidlem37 41042 stoweidlem38 41043 stoweidlem40 41045 stoweidlem41 41046 stoweidlem43 41048 stoweidlem44 41049 stoweidlem46 41051 stoweidlem5 41010 stoweidlem50 41055 stoweidlem52 41057 stoweidlem53 41058 stoweidlem55 41060 stoweidlem56 41061 |
[BrosowskiDeutsh] p. 90 | Lemma 1
| stoweidlem23 41028 stoweidlem24 41029 stoweidlem27 41032 stoweidlem28 41033 stoweidlem30 41035 |
[BrosowskiDeutsh] p.
91 | Proof | stoweidlem34 41039 stoweidlem59 41064 stoweidlem60 41065 |
[BrosowskiDeutsh] p. 91 | Lemma
1 | stoweidlem45 41050 stoweidlem49 41054 stoweidlem7 41012 |
[BrosowskiDeutsh] p. 91 | Lemma
2 | stoweidlem31 41036 stoweidlem39 41044 stoweidlem42 41047 stoweidlem48 41053 stoweidlem51 41056 stoweidlem54 41059 stoweidlem57 41062 stoweidlem58 41063 |
[BrosowskiDeutsh] p. 91 | Lemma 1
| stoweidlem25 41030 |
[BrosowskiDeutsh] p. 91 | Lemma
proves that the function ` ` (as defined | stoweidlem17 41022 |
[BrosowskiDeutsh] p.
92 | Proof | stoweidlem11 41016 stoweidlem13 41018 stoweidlem26 41031 stoweidlem61 41066 |
[BrosowskiDeutsh] p. 92 | Lemma
2 | stoweidlem18 41023 |
[Bruck] p.
1 | Section I.1 | df-clintop 42697 df-mgm 17602 df-mgm2 42716 |
[Bruck] p. 23 | Section
II.1 | df-sgrp 17644 df-sgrp2 42718 |
[Bruck] p. 28 | Theorem
3.2 | dfgrp3 17875 |
[ChoquetDD] p.
2 | Definition of mapping | df-mpt 4955 |
[Church] p. 129 | Section
II.24 | df-ifp 1090 dfifp2 1091 |
[Clemente] p.
10 | Definition IT | natded 27814 |
[Clemente] p.
10 | Definition I` `m,n | natded 27814 |
[Clemente] p.
11 | Definition E=>m,n | natded 27814 |
[Clemente] p.
11 | Definition I=>m,n | natded 27814 |
[Clemente] p.
11 | Definition E` `(1) | natded 27814 |
[Clemente] p.
11 | Definition E` `(2) | natded 27814 |
[Clemente] p.
12 | Definition E` `m,n,p | natded 27814 |
[Clemente] p.
12 | Definition I` `n(1) | natded 27814 |
[Clemente] p.
12 | Definition I` `n(2) | natded 27814 |
[Clemente] p.
13 | Definition I` `m,n,p | natded 27814 |
[Clemente] p. 14 | Proof
5.11 | natded 27814 |
[Clemente] p.
14 | Definition E` `n | natded 27814 |
[Clemente] p.
15 | Theorem 5.2 | ex-natded5.2-2 27816 ex-natded5.2 27815 |
[Clemente] p.
16 | Theorem 5.3 | ex-natded5.3-2 27819 ex-natded5.3 27818 |
[Clemente] p.
18 | Theorem 5.5 | ex-natded5.5 27821 |
[Clemente] p.
19 | Theorem 5.7 | ex-natded5.7-2 27823 ex-natded5.7 27822 |
[Clemente] p.
20 | Theorem 5.8 | ex-natded5.8-2 27825 ex-natded5.8 27824 |
[Clemente] p.
20 | Theorem 5.13 | ex-natded5.13-2 27827 ex-natded5.13 27826 |
[Clemente] p.
32 | Definition I` `n | natded 27814 |
[Clemente] p.
32 | Definition E` `m,n,p,a | natded 27814 |
[Clemente] p.
32 | Definition E` `n,t | natded 27814 |
[Clemente] p.
32 | Definition I` `n,t | natded 27814 |
[Clemente] p.
43 | Theorem 9.20 | ex-natded9.20 27828 |
[Clemente] p.
45 | Theorem 9.20 | ex-natded9.20-2 27829 |
[Clemente] p.
45 | Theorem 9.26 | ex-natded9.26-2 27831 ex-natded9.26 27830 |
[Cohen] p.
301 | Remark | relogoprlem 24743 |
[Cohen] p. 301 | Property
2 | relogmul 24744 relogmuld 24777 |
[Cohen] p. 301 | Property
3 | relogdiv 24745 relogdivd 24778 |
[Cohen] p. 301 | Property
4 | relogexp 24748 |
[Cohen] p. 301 | Property
1a | log1 24738 |
[Cohen] p. 301 | Property
1b | loge 24739 |
[Cohen4] p.
348 | Observation | relogbcxpb 24934 |
[Cohen4] p.
349 | Property | relogbf 24938 |
[Cohen4] p.
352 | Definition | elogb 24917 |
[Cohen4] p. 361 | Property
2 | relogbmul 24924 |
[Cohen4] p. 361 | Property
3 | logbrec 24929 relogbdiv 24926 |
[Cohen4] p. 361 | Property
4 | relogbreexp 24922 |
[Cohen4] p. 361 | Property
6 | relogbexp 24927 |
[Cohen4] p. 361 | Property
1(a) | logbid1 24915 |
[Cohen4] p. 361 | Property
1(b) | logb1 24916 |
[Cohen4] p.
367 | Property | logbchbase 24918 |
[Cohen4] p. 377 | Property
2 | logblt 24931 |
[Cohn] p.
4 | Proposition 1.1.5 | sxbrsigalem1 30888 sxbrsigalem4 30890 |
[Cohn] p. 81 | Section
II.5 | acsdomd 17541 acsinfd 17540 acsinfdimd 17542 acsmap2d 17539 acsmapd 17538 |
[Cohn] p.
143 | Example 5.1.1 | sxbrsiga 30893 |
[Connell] p.
57 | Definition | df-scmat 20672 df-scmatalt 43049 |
[CormenLeisersonRivest] p.
33 | Equation 2.4 | fldiv2 12962 |
[Crawley] p.
1 | Definition of poset | df-poset 17306 |
[Crawley] p.
107 | Theorem 13.2 | hlsupr 35456 |
[Crawley] p.
110 | Theorem 13.3 | arglem1N 36260 dalaw 35956 |
[Crawley] p.
111 | Theorem 13.4 | hlathil 38031 |
[Crawley] p.
111 | Definition of set W | df-watsN 36060 |
[Crawley] p.
111 | Definition of dilation | df-dilN 36176 df-ldil 36174 isldil 36180 |
[Crawley] p.
111 | Definition of translation | df-ltrn 36175 df-trnN 36177 isltrn 36189 ltrnu 36191 |
[Crawley] p.
112 | Lemma A | cdlema1N 35861 cdlema2N 35862 exatleN 35474 |
[Crawley] p.
112 | Lemma B | 1cvrat 35546 cdlemb 35864 cdlemb2 36111 cdlemb3 36676 idltrn 36220 l1cvat 35125 lhpat 36113 lhpat2 36115 lshpat 35126 ltrnel 36209 ltrnmw 36221 |
[Crawley] p.
112 | Lemma C | cdlemc1 36261 cdlemc2 36262 ltrnnidn 36244 trlat 36239 trljat1 36236 trljat2 36237 trljat3 36238 trlne 36255 trlnidat 36243 trlnle 36256 |
[Crawley] p.
112 | Definition of automorphism | df-pautN 36061 |
[Crawley] p.
113 | Lemma C | cdlemc 36267 cdlemc3 36263 cdlemc4 36264 |
[Crawley] p.
113 | Lemma D | cdlemd 36277 cdlemd1 36268 cdlemd2 36269 cdlemd3 36270 cdlemd4 36271 cdlemd5 36272 cdlemd6 36273 cdlemd7 36274 cdlemd8 36275 cdlemd9 36276 cdleme31sde 36455 cdleme31se 36452 cdleme31se2 36453 cdleme31snd 36456 cdleme32a 36511 cdleme32b 36512 cdleme32c 36513 cdleme32d 36514 cdleme32e 36515 cdleme32f 36516 cdleme32fva 36507 cdleme32fva1 36508 cdleme32fvcl 36510 cdleme32le 36517 cdleme48fv 36569 cdleme4gfv 36577 cdleme50eq 36611 cdleme50f 36612 cdleme50f1 36613 cdleme50f1o 36616 cdleme50laut 36617 cdleme50ldil 36618 cdleme50lebi 36610 cdleme50rn 36615 cdleme50rnlem 36614 cdlemeg49le 36581 cdlemeg49lebilem 36609 |
[Crawley] p.
113 | Lemma E | cdleme 36630 cdleme00a 36279 cdleme01N 36291 cdleme02N 36292 cdleme0a 36281 cdleme0aa 36280 cdleme0b 36282 cdleme0c 36283 cdleme0cp 36284 cdleme0cq 36285 cdleme0dN 36286 cdleme0e 36287 cdleme0ex1N 36293 cdleme0ex2N 36294 cdleme0fN 36288 cdleme0gN 36289 cdleme0moN 36295 cdleme1 36297 cdleme10 36324 cdleme10tN 36328 cdleme11 36340 cdleme11a 36330 cdleme11c 36331 cdleme11dN 36332 cdleme11e 36333 cdleme11fN 36334 cdleme11g 36335 cdleme11h 36336 cdleme11j 36337 cdleme11k 36338 cdleme11l 36339 cdleme12 36341 cdleme13 36342 cdleme14 36343 cdleme15 36348 cdleme15a 36344 cdleme15b 36345 cdleme15c 36346 cdleme15d 36347 cdleme16 36355 cdleme16aN 36329 cdleme16b 36349 cdleme16c 36350 cdleme16d 36351 cdleme16e 36352 cdleme16f 36353 cdleme16g 36354 cdleme19a 36373 cdleme19b 36374 cdleme19c 36375 cdleme19d 36376 cdleme19e 36377 cdleme19f 36378 cdleme1b 36296 cdleme2 36298 cdleme20aN 36379 cdleme20bN 36380 cdleme20c 36381 cdleme20d 36382 cdleme20e 36383 cdleme20f 36384 cdleme20g 36385 cdleme20h 36386 cdleme20i 36387 cdleme20j 36388 cdleme20k 36389 cdleme20l 36392 cdleme20l1 36390 cdleme20l2 36391 cdleme20m 36393 cdleme20y 36372 cdleme20zN 36371 cdleme21 36407 cdleme21d 36400 cdleme21e 36401 cdleme22a 36410 cdleme22aa 36409 cdleme22b 36411 cdleme22cN 36412 cdleme22d 36413 cdleme22e 36414 cdleme22eALTN 36415 cdleme22f 36416 cdleme22f2 36417 cdleme22g 36418 cdleme23a 36419 cdleme23b 36420 cdleme23c 36421 cdleme26e 36429 cdleme26eALTN 36431 cdleme26ee 36430 cdleme26f 36433 cdleme26f2 36435 cdleme26f2ALTN 36434 cdleme26fALTN 36432 cdleme27N 36439 cdleme27a 36437 cdleme27cl 36436 cdleme28c 36442 cdleme3 36307 cdleme30a 36448 cdleme31fv 36460 cdleme31fv1 36461 cdleme31fv1s 36462 cdleme31fv2 36463 cdleme31id 36464 cdleme31sc 36454 cdleme31sdnN 36457 cdleme31sn 36450 cdleme31sn1 36451 cdleme31sn1c 36458 cdleme31sn2 36459 cdleme31so 36449 cdleme35a 36518 cdleme35b 36520 cdleme35c 36521 cdleme35d 36522 cdleme35e 36523 cdleme35f 36524 cdleme35fnpq 36519 cdleme35g 36525 cdleme35h 36526 cdleme35h2 36527 cdleme35sn2aw 36528 cdleme35sn3a 36529 cdleme36a 36530 cdleme36m 36531 cdleme37m 36532 cdleme38m 36533 cdleme38n 36534 cdleme39a 36535 cdleme39n 36536 cdleme3b 36299 cdleme3c 36300 cdleme3d 36301 cdleme3e 36302 cdleme3fN 36303 cdleme3fa 36306 cdleme3g 36304 cdleme3h 36305 cdleme4 36308 cdleme40m 36537 cdleme40n 36538 cdleme40v 36539 cdleme40w 36540 cdleme41fva11 36547 cdleme41sn3aw 36544 cdleme41sn4aw 36545 cdleme41snaw 36546 cdleme42a 36541 cdleme42b 36548 cdleme42c 36542 cdleme42d 36543 cdleme42e 36549 cdleme42f 36550 cdleme42g 36551 cdleme42h 36552 cdleme42i 36553 cdleme42k 36554 cdleme42ke 36555 cdleme42keg 36556 cdleme42mN 36557 cdleme42mgN 36558 cdleme43aN 36559 cdleme43bN 36560 cdleme43cN 36561 cdleme43dN 36562 cdleme5 36310 cdleme50ex 36629 cdleme50ltrn 36627 cdleme51finvN 36626 cdleme51finvfvN 36625 cdleme51finvtrN 36628 cdleme6 36311 cdleme7 36319 cdleme7a 36313 cdleme7aa 36312 cdleme7b 36314 cdleme7c 36315 cdleme7d 36316 cdleme7e 36317 cdleme7ga 36318 cdleme8 36320 cdleme8tN 36325 cdleme9 36323 cdleme9a 36321 cdleme9b 36322 cdleme9tN 36327 cdleme9taN 36326 cdlemeda 36368 cdlemedb 36367 cdlemednpq 36369 cdlemednuN 36370 cdlemefr27cl 36473 cdlemefr32fva1 36480 cdlemefr32fvaN 36479 cdlemefrs32fva 36470 cdlemefrs32fva1 36471 cdlemefs27cl 36483 cdlemefs32fva1 36493 cdlemefs32fvaN 36492 cdlemesner 36366 cdlemeulpq 36290 |
[Crawley] p.
114 | Lemma E | 4atex 36146 4atexlem7 36145 cdleme0nex 36360 cdleme17a 36356 cdleme17c 36358 cdleme17d 36568 cdleme17d1 36359 cdleme17d2 36565 cdleme18a 36361 cdleme18b 36362 cdleme18c 36363 cdleme18d 36365 cdleme4a 36309 |
[Crawley] p.
115 | Lemma E | cdleme21a 36395 cdleme21at 36398 cdleme21b 36396 cdleme21c 36397 cdleme21ct 36399 cdleme21f 36402 cdleme21g 36403 cdleme21h 36404 cdleme21i 36405 cdleme22gb 36364 |
[Crawley] p.
116 | Lemma F | cdlemf 36633 cdlemf1 36631 cdlemf2 36632 |
[Crawley] p.
116 | Lemma G | cdlemftr1 36637 cdlemg16 36727 cdlemg28 36774 cdlemg28a 36763 cdlemg28b 36773 cdlemg3a 36667 cdlemg42 36799 cdlemg43 36800 cdlemg44 36803 cdlemg44a 36801 cdlemg46 36805 cdlemg47 36806 cdlemg9 36704 ltrnco 36789 ltrncom 36808 tgrpabl 36821 trlco 36797 |
[Crawley] p.
116 | Definition of G | df-tgrp 36813 |
[Crawley] p.
117 | Lemma G | cdlemg17 36747 cdlemg17b 36732 |
[Crawley] p.
117 | Definition of E | df-edring-rN 36826 df-edring 36827 |
[Crawley] p.
117 | Definition of trace-preserving endomorphism | istendo 36830 |
[Crawley] p.
118 | Remark | tendopltp 36850 |
[Crawley] p.
118 | Lemma H | cdlemh 36887 cdlemh1 36885 cdlemh2 36886 |
[Crawley] p.
118 | Lemma I | cdlemi 36890 cdlemi1 36888 cdlemi2 36889 |
[Crawley] p.
118 | Lemma J | cdlemj1 36891 cdlemj2 36892 cdlemj3 36893 tendocan 36894 |
[Crawley] p.
118 | Lemma K | cdlemk 37044 cdlemk1 36901 cdlemk10 36913 cdlemk11 36919 cdlemk11t 37016 cdlemk11ta 36999 cdlemk11tb 37001 cdlemk11tc 37015 cdlemk11u-2N 36959 cdlemk11u 36941 cdlemk12 36920 cdlemk12u-2N 36960 cdlemk12u 36942 cdlemk13-2N 36946 cdlemk13 36922 cdlemk14-2N 36948 cdlemk14 36924 cdlemk15-2N 36949 cdlemk15 36925 cdlemk16-2N 36950 cdlemk16 36927 cdlemk16a 36926 cdlemk17-2N 36951 cdlemk17 36928 cdlemk18-2N 36956 cdlemk18-3N 36970 cdlemk18 36938 cdlemk19-2N 36957 cdlemk19 36939 cdlemk19u 37040 cdlemk1u 36929 cdlemk2 36902 cdlemk20-2N 36962 cdlemk20 36944 cdlemk21-2N 36961 cdlemk21N 36943 cdlemk22-3 36971 cdlemk22 36963 cdlemk23-3 36972 cdlemk24-3 36973 cdlemk25-3 36974 cdlemk26-3 36976 cdlemk26b-3 36975 cdlemk27-3 36977 cdlemk28-3 36978 cdlemk29-3 36981 cdlemk3 36903 cdlemk30 36964 cdlemk31 36966 cdlemk32 36967 cdlemk33N 36979 cdlemk34 36980 cdlemk35 36982 cdlemk36 36983 cdlemk37 36984 cdlemk38 36985 cdlemk39 36986 cdlemk39u 37038 cdlemk4 36904 cdlemk41 36990 cdlemk42 37011 cdlemk42yN 37014 cdlemk43N 37033 cdlemk45 37017 cdlemk46 37018 cdlemk47 37019 cdlemk48 37020 cdlemk49 37021 cdlemk5 36906 cdlemk50 37022 cdlemk51 37023 cdlemk52 37024 cdlemk53 37027 cdlemk54 37028 cdlemk55 37031 cdlemk55u 37036 cdlemk56 37041 cdlemk5a 36905 cdlemk5auN 36930 cdlemk5u 36931 cdlemk6 36907 cdlemk6u 36932 cdlemk7 36918 cdlemk7u-2N 36958 cdlemk7u 36940 cdlemk8 36908 cdlemk9 36909 cdlemk9bN 36910 cdlemki 36911 cdlemkid 37006 cdlemkj-2N 36952 cdlemkj 36933 cdlemksat 36916 cdlemksel 36915 cdlemksv 36914 cdlemksv2 36917 cdlemkuat 36936 cdlemkuel-2N 36954 cdlemkuel-3 36968 cdlemkuel 36935 cdlemkuv-2N 36953 cdlemkuv2-2 36955 cdlemkuv2-3N 36969 cdlemkuv2 36937 cdlemkuvN 36934 cdlemkvcl 36912 cdlemky 36996 cdlemkyyN 37032 tendoex 37045 |
[Crawley] p.
120 | Remark | dva1dim 37055 |
[Crawley] p.
120 | Lemma L | cdleml1N 37046 cdleml2N 37047 cdleml3N 37048 cdleml4N 37049 cdleml5N 37050 cdleml6 37051 cdleml7 37052 cdleml8 37053 cdleml9 37054 dia1dim 37131 |
[Crawley] p.
120 | Lemma M | dia11N 37118 diaf11N 37119 dialss 37116 diaord 37117 dibf11N 37231 djajN 37207 |
[Crawley] p.
120 | Definition of isomorphism map | diaval 37102 |
[Crawley] p.
121 | Lemma M | cdlemm10N 37188 dia2dimlem1 37134 dia2dimlem2 37135 dia2dimlem3 37136 dia2dimlem4 37137 dia2dimlem5 37138 diaf1oN 37200 diarnN 37199 dvheveccl 37182 dvhopN 37186 |
[Crawley] p.
121 | Lemma N | cdlemn 37282 cdlemn10 37276 cdlemn11 37281 cdlemn11a 37277 cdlemn11b 37278 cdlemn11c 37279 cdlemn11pre 37280 cdlemn2 37265 cdlemn2a 37266 cdlemn3 37267 cdlemn4 37268 cdlemn4a 37269 cdlemn5 37271 cdlemn5pre 37270 cdlemn6 37272 cdlemn7 37273 cdlemn8 37274 cdlemn9 37275 diclspsn 37264 |
[Crawley] p.
121 | Definition of phi(q) | df-dic 37243 |
[Crawley] p.
122 | Lemma N | dih11 37335 dihf11 37337 dihjust 37287 dihjustlem 37286 dihord 37334 dihord1 37288 dihord10 37293 dihord11b 37292 dihord11c 37294 dihord2 37297 dihord2a 37289 dihord2b 37290 dihord2cN 37291 dihord2pre 37295 dihord2pre2 37296 dihordlem6 37283 dihordlem7 37284 dihordlem7b 37285 |
[Crawley] p.
122 | Definition of isomorphism map | dihffval 37300 dihfval 37301 dihval 37302 |
[Diestel] p. 3 | Section
1.1 | df-cusgr 26717 df-nbgr 26637 |
[Diestel] p. 4 | Section
1.1 | df-subgr 26572 uhgrspan1 26607 uhgrspansubgr 26595 |
[Diestel] p.
5 | Proposition 1.2.1 | fusgrvtxdgonume 26859 vtxdgoddnumeven 26858 |
[Diestel] p. 27 | Section
1.10 | df-ushgr 26364 |
[Eisenberg] p.
67 | Definition 5.3 | df-dif 3801 |
[Eisenberg] p.
82 | Definition 6.3 | dfom3 8828 |
[Eisenberg] p.
125 | Definition 8.21 | df-map 8129 |
[Eisenberg] p.
216 | Example 13.2(4) | omenps 8836 |
[Eisenberg] p.
310 | Theorem 19.8 | cardprc 9126 |
[Eisenberg] p.
310 | Corollary 19.7(2) | cardsdom 9699 |
[Enderton] p. 18 | Axiom
of Empty Set | axnul 5014 |
[Enderton] p.
19 | Definition | df-tp 4404 |
[Enderton] p.
26 | Exercise 5 | unissb 4693 |
[Enderton] p.
26 | Exercise 10 | pwel 5143 |
[Enderton] p.
28 | Exercise 7(b) | pwun 5250 |
[Enderton] p.
30 | Theorem "Distributive laws" | iinin1 4813 iinin2 4812 iinun2 4808 iunin1 4807 iunin1f 29918 iunin2 4806 uniin1 29911 uniin2 29912 |
[Enderton] p.
31 | Theorem "De Morgan's laws" | iindif2 4811 iundif2 4809 |
[Enderton] p.
32 | Exercise 20 | unineq 4109 |
[Enderton] p.
33 | Exercise 23 | iinuni 4832 |
[Enderton] p.
33 | Exercise 25 | iununi 4833 |
[Enderton] p.
33 | Exercise 24(a) | iinpw 4840 |
[Enderton] p.
33 | Exercise 24(b) | iunpw 7244 iunpwss 4841 |
[Enderton] p.
36 | Definition | opthwiener 5202 |
[Enderton] p.
38 | Exercise 6(a) | unipw 5141 |
[Enderton] p.
38 | Exercise 6(b) | pwuni 4698 |
[Enderton] p. 41 | Lemma
3D | opeluu 5161 rnex 7367
rnexg 7364 |
[Enderton] p.
41 | Exercise 8 | dmuni 5570 rnuni 5789 |
[Enderton] p.
42 | Definition of a function | dffun7 6154 dffun8 6155 |
[Enderton] p.
43 | Definition of function value | funfv2 6517 |
[Enderton] p.
43 | Definition of single-rooted | funcnv 6195 |
[Enderton] p.
44 | Definition (d) | dfima2 5713 dfima3 5714 |
[Enderton] p.
47 | Theorem 3H | fvco2 6524 |
[Enderton] p. 49 | Axiom
of Choice (first form) | ac7 9617 ac7g 9618
df-ac 9259 dfac2 9274 dfac2a 9272 dfac2b 9273 dfac3 9264 dfac7 9276 |
[Enderton] p.
50 | Theorem 3K(a) | imauni 6764 |
[Enderton] p.
52 | Definition | df-map 8129 |
[Enderton] p.
53 | Exercise 21 | coass 5899 |
[Enderton] p.
53 | Exercise 27 | dmco 5888 |
[Enderton] p.
53 | Exercise 14(a) | funin 6202 |
[Enderton] p.
53 | Exercise 22(a) | imass2 5746 |
[Enderton] p.
54 | Remark | ixpf 8203 ixpssmap 8215 |
[Enderton] p.
54 | Definition of infinite Cartesian product | df-ixp 8182 |
[Enderton] p. 55 | Axiom
of Choice (second form) | ac9 9627 ac9s 9637 |
[Enderton]
p. 56 | Theorem 3M | eqvrelref 34895 erref 8034 |
[Enderton]
p. 57 | Lemma 3N | eqvrelthi 34898 erthi 8063 |
[Enderton] p.
57 | Definition | df-ec 8016 |
[Enderton] p.
58 | Definition | df-qs 8020 |
[Enderton] p.
61 | Exercise 35 | df-ec 8016 |
[Enderton] p.
65 | Exercise 56(a) | dmun 5567 |
[Enderton] p.
68 | Definition of successor | df-suc 5973 |
[Enderton] p.
71 | Definition | df-tr 4978 dftr4 4982 |
[Enderton] p.
72 | Theorem 4E | unisuc 6043 |
[Enderton] p.
73 | Exercise 6 | unisuc 6043 |
[Enderton] p.
73 | Exercise 5(a) | truni 4991 |
[Enderton] p.
73 | Exercise 5(b) | trint 4993 trintALT 39930 |
[Enderton] p.
79 | Theorem 4I(A1) | nna0 7956 |
[Enderton] p.
79 | Theorem 4I(A2) | nnasuc 7958 onasuc 7880 |
[Enderton] p.
79 | Definition of operation value | df-ov 6913 |
[Enderton] p.
80 | Theorem 4J(A1) | nnm0 7957 |
[Enderton] p.
80 | Theorem 4J(A2) | nnmsuc 7959 onmsuc 7881 |
[Enderton] p.
81 | Theorem 4K(1) | nnaass 7974 |
[Enderton] p.
81 | Theorem 4K(2) | nna0r 7961 nnacom 7969 |
[Enderton] p.
81 | Theorem 4K(3) | nndi 7975 |
[Enderton] p.
81 | Theorem 4K(4) | nnmass 7976 |
[Enderton] p.
81 | Theorem 4K(5) | nnmcom 7978 |
[Enderton] p.
82 | Exercise 16 | nnm0r 7962 nnmsucr 7977 |
[Enderton] p.
88 | Exercise 23 | nnaordex 7990 |
[Enderton] p.
129 | Definition | df-en 8229 |
[Enderton] p.
132 | Theorem 6B(b) | canth 6868 |
[Enderton] p.
133 | Exercise 1 | xpomen 9158 |
[Enderton] p.
133 | Exercise 2 | qnnen 15323 |
[Enderton] p.
134 | Theorem (Pigeonhole Principle) | php 8419 |
[Enderton] p.
135 | Corollary 6C | php3 8421 |
[Enderton] p.
136 | Corollary 6E | nneneq 8418 |
[Enderton] p.
136 | Corollary 6D(a) | pssinf 8445 |
[Enderton] p.
136 | Corollary 6D(b) | ominf 8447 |
[Enderton] p.
137 | Lemma 6F | pssnn 8453 |
[Enderton] p.
138 | Corollary 6G | ssfi 8455 |
[Enderton] p.
139 | Theorem 6H(c) | mapen 8399 |
[Enderton] p.
142 | Theorem 6I(3) | xpcdaen 9327 |
[Enderton] p.
142 | Theorem 6I(4) | mapcdaen 9328 |
[Enderton] p.
143 | Theorem 6J | cda0en 9323 cda1en 9319 |
[Enderton] p.
144 | Exercise 13 | iunfi 8529 unifi 8530 unifi2 8531 |
[Enderton] p.
144 | Corollary 6K | undif2 4269 unfi 8502
unfi2 8504 |
[Enderton] p.
145 | Figure 38 | ffoss 7394 |
[Enderton] p.
145 | Definition | df-dom 8230 |
[Enderton] p.
146 | Example 1 | domen 8241 domeng 8242 |
[Enderton] p.
146 | Example 3 | nndomo 8429 nnsdom 8835 nnsdomg 8494 |
[Enderton] p.
149 | Theorem 6L(a) | cdadom2 9331 |
[Enderton] p.
149 | Theorem 6L(c) | mapdom1 8400 xpdom1 8334 xpdom1g 8332 xpdom2g 8331 |
[Enderton] p.
149 | Theorem 6L(d) | mapdom2 8406 |
[Enderton] p.
151 | Theorem 6M | zorn 9651 zorng 9648 |
[Enderton] p.
151 | Theorem 6M(4) | ac8 9636 dfac5 9271 |
[Enderton] p.
159 | Theorem 6Q | unictb 9719 |
[Enderton] p.
164 | Example | infdif 9353 |
[Enderton] p.
168 | Definition | df-po 5265 |
[Enderton] p.
192 | Theorem 7M(a) | oneli 6074 |
[Enderton] p.
192 | Theorem 7M(b) | ontr1 6013 |
[Enderton] p.
192 | Theorem 7M(c) | onirri 6073 |
[Enderton] p.
193 | Corollary 7N(b) | 0elon 6020 |
[Enderton] p.
193 | Corollary 7N(c) | onsuci 7304 |
[Enderton] p.
193 | Corollary 7N(d) | ssonunii 7253 |
[Enderton] p.
194 | Remark | onprc 7250 |
[Enderton] p.
194 | Exercise 16 | suc11 6070 |
[Enderton] p.
197 | Definition | df-card 9085 |
[Enderton] p.
197 | Theorem 7P | carden 9695 |
[Enderton] p.
200 | Exercise 25 | tfis 7320 |
[Enderton] p.
202 | Lemma 7T | r1tr 8923 |
[Enderton] p.
202 | Definition | df-r1 8911 |
[Enderton] p.
202 | Theorem 7Q | r1val1 8933 |
[Enderton] p.
204 | Theorem 7V(b) | rankval4 9014 |
[Enderton] p.
206 | Theorem 7X(b) | en2lp 8786 |
[Enderton] p.
207 | Exercise 30 | rankpr 9004 rankprb 8998 rankpw 8990 rankpwi 8970 rankuniss 9013 |
[Enderton] p.
207 | Exercise 34 | opthreg 8797 |
[Enderton] p.
208 | Exercise 35 | suc11reg 8800 |
[Enderton] p.
212 | Definition of aleph | alephval3 9253 |
[Enderton] p.
213 | Theorem 8A(a) | alephord2 9219 |
[Enderton] p.
213 | Theorem 8A(b) | cardalephex 9233 |
[Enderton] p.
218 | Theorem Schema 8E | onfununi 7709 |
[Enderton] p.
222 | Definition of kard | karden 9042 kardex 9041 |
[Enderton] p.
238 | Theorem 8R | oeoa 7949 |
[Enderton] p.
238 | Theorem 8S | oeoe 7951 |
[Enderton] p.
240 | Exercise 25 | oarec 7914 |
[Enderton] p.
257 | Definition of cofinality | cflm 9394 |
[FaureFrolicher] p.
57 | Definition 3.1.9 | mreexd 16662 |
[FaureFrolicher] p.
83 | Definition 4.1.1 | df-mri 16608 |
[FaureFrolicher] p.
83 | Proposition 4.1.3 | acsfiindd 17537 mrieqv2d 16659 mrieqvd 16658 |
[FaureFrolicher] p.
84 | Lemma 4.1.5 | mreexmrid 16663 |
[FaureFrolicher] p.
86 | Proposition 4.2.1 | mreexexd 16668 mreexexlem2d 16665 |
[FaureFrolicher] p.
87 | Theorem 4.2.2 | acsexdimd 17543 mreexfidimd 16670 |
[Frege1879]
p. 11 | Statement | df3or2 38896 |
[Frege1879]
p. 12 | Statement | df3an2 38897 dfxor4 38894 dfxor5 38895 |
[Frege1879]
p. 26 | Axiom 1 | ax-frege1 38919 |
[Frege1879]
p. 26 | Axiom 2 | ax-frege2 38920 |
[Frege1879] p.
26 | Proposition 1 | ax-1 6 |
[Frege1879] p.
26 | Proposition 2 | ax-2 7 |
[Frege1879]
p. 29 | Proposition 3 | frege3 38924 |
[Frege1879]
p. 31 | Proposition 4 | frege4 38928 |
[Frege1879]
p. 32 | Proposition 5 | frege5 38929 |
[Frege1879]
p. 33 | Proposition 6 | frege6 38935 |
[Frege1879]
p. 34 | Proposition 7 | frege7 38937 |
[Frege1879]
p. 35 | Axiom 8 | ax-frege8 38938 axfrege8 38936 |
[Frege1879] p.
35 | Proposition 8 | pm2.04 90 wl-luk-pm2.04 33809 |
[Frege1879]
p. 35 | Proposition 9 | frege9 38941 |
[Frege1879]
p. 36 | Proposition 10 | frege10 38949 |
[Frege1879]
p. 36 | Proposition 11 | frege11 38943 |
[Frege1879]
p. 37 | Proposition 12 | frege12 38942 |
[Frege1879]
p. 37 | Proposition 13 | frege13 38951 |
[Frege1879]
p. 37 | Proposition 14 | frege14 38952 |
[Frege1879]
p. 38 | Proposition 15 | frege15 38955 |
[Frege1879]
p. 38 | Proposition 16 | frege16 38945 |
[Frege1879]
p. 39 | Proposition 17 | frege17 38950 |
[Frege1879]
p. 39 | Proposition 18 | frege18 38947 |
[Frege1879]
p. 39 | Proposition 19 | frege19 38953 |
[Frege1879]
p. 40 | Proposition 20 | frege20 38957 |
[Frege1879]
p. 40 | Proposition 21 | frege21 38956 |
[Frege1879]
p. 41 | Proposition 22 | frege22 38948 |
[Frege1879]
p. 42 | Proposition 23 | frege23 38954 |
[Frege1879]
p. 42 | Proposition 24 | frege24 38944 |
[Frege1879]
p. 42 | Proposition 25 | frege25 38946 rp-frege25 38934 |
[Frege1879]
p. 42 | Proposition 26 | frege26 38939 |
[Frege1879]
p. 43 | Axiom 28 | ax-frege28 38959 |
[Frege1879]
p. 43 | Proposition 27 | frege27 38940 |
[Frege1879] p.
43 | Proposition 28 | con3 151 |
[Frege1879]
p. 43 | Proposition 29 | frege29 38960 |
[Frege1879]
p. 44 | Axiom 31 | ax-frege31 38963 axfrege31 38962 |
[Frege1879]
p. 44 | Proposition 30 | frege30 38961 |
[Frege1879] p.
44 | Proposition 31 | notnotr 128 |
[Frege1879]
p. 44 | Proposition 32 | frege32 38964 |
[Frege1879]
p. 44 | Proposition 33 | frege33 38965 |
[Frege1879]
p. 45 | Proposition 34 | frege34 38966 |
[Frege1879]
p. 45 | Proposition 35 | frege35 38967 |
[Frege1879]
p. 45 | Proposition 36 | frege36 38968 |
[Frege1879]
p. 46 | Proposition 37 | frege37 38969 |
[Frege1879]
p. 46 | Proposition 38 | frege38 38970 |
[Frege1879]
p. 46 | Proposition 39 | frege39 38971 |
[Frege1879]
p. 46 | Proposition 40 | frege40 38972 |
[Frege1879]
p. 47 | Axiom 41 | ax-frege41 38974 axfrege41 38973 |
[Frege1879] p.
47 | Proposition 41 | notnot 139 |
[Frege1879]
p. 47 | Proposition 42 | frege42 38975 |
[Frege1879]
p. 47 | Proposition 43 | frege43 38976 |
[Frege1879]
p. 47 | Proposition 44 | frege44 38977 |
[Frege1879]
p. 47 | Proposition 45 | frege45 38978 |
[Frege1879]
p. 48 | Proposition 46 | frege46 38979 |
[Frege1879]
p. 48 | Proposition 47 | frege47 38980 |
[Frege1879]
p. 49 | Proposition 48 | frege48 38981 |
[Frege1879]
p. 49 | Proposition 49 | frege49 38982 |
[Frege1879]
p. 49 | Proposition 50 | frege50 38983 |
[Frege1879]
p. 50 | Axiom 52 | ax-frege52a 38986 ax-frege52c 39017 frege52aid 38987 frege52b 39018 |
[Frege1879]
p. 50 | Axiom 54 | ax-frege54a 38991 ax-frege54c 39021 frege54b 39022 |
[Frege1879]
p. 50 | Proposition 51 | frege51 38984 |
[Frege1879] p.
50 | Proposition 52 | dfsbcq 3664 |
[Frege1879]
p. 50 | Proposition 53 | frege53a 38989 frege53aid 38988 frege53b 39019 frege53c 39043 |
[Frege1879] p.
50 | Proposition 54 | biid 253 eqid 2825 |
[Frege1879]
p. 50 | Proposition 55 | frege55a 38997 frege55aid 38994 frege55b 39026 frege55c 39047 frege55cor1a 38998 frege55lem2a 38996 frege55lem2b 39025 frege55lem2c 39046 |
[Frege1879]
p. 50 | Proposition 56 | frege56a 39000 frege56aid 38999 frege56b 39027 frege56c 39048 |
[Frege1879]
p. 51 | Axiom 58 | ax-frege58a 39004 ax-frege58b 39030 frege58bid 39031 frege58c 39050 |
[Frege1879]
p. 51 | Proposition 57 | frege57a 39002 frege57aid 39001 frege57b 39028 frege57c 39049 |
[Frege1879] p.
51 | Proposition 58 | spsbc 3675 |
[Frege1879]
p. 51 | Proposition 59 | frege59a 39006 frege59b 39033 frege59c 39051 |
[Frege1879]
p. 52 | Proposition 60 | frege60a 39007 frege60b 39034 frege60c 39052 |
[Frege1879]
p. 52 | Proposition 61 | frege61a 39008 frege61b 39035 frege61c 39053 |
[Frege1879]
p. 52 | Proposition 62 | frege62a 39009 frege62b 39036 frege62c 39054 |
[Frege1879]
p. 52 | Proposition 63 | frege63a 39010 frege63b 39037 frege63c 39055 |
[Frege1879]
p. 53 | Proposition 64 | frege64a 39011 frege64b 39038 frege64c 39056 |
[Frege1879]
p. 53 | Proposition 65 | frege65a 39012 frege65b 39039 frege65c 39057 |
[Frege1879]
p. 54 | Proposition 66 | frege66a 39013 frege66b 39040 frege66c 39058 |
[Frege1879]
p. 54 | Proposition 67 | frege67a 39014 frege67b 39041 frege67c 39059 |
[Frege1879]
p. 54 | Proposition 68 | frege68a 39015 frege68b 39042 frege68c 39060 |
[Frege1879]
p. 55 | Definition 69 | dffrege69 39061 |
[Frege1879]
p. 58 | Proposition 70 | frege70 39062 |
[Frege1879]
p. 59 | Proposition 71 | frege71 39063 |
[Frege1879]
p. 59 | Proposition 72 | frege72 39064 |
[Frege1879]
p. 59 | Proposition 73 | frege73 39065 |
[Frege1879]
p. 60 | Definition 76 | dffrege76 39068 |
[Frege1879]
p. 60 | Proposition 74 | frege74 39066 |
[Frege1879]
p. 60 | Proposition 75 | frege75 39067 |
[Frege1879]
p. 62 | Proposition 77 | frege77 39069 frege77d 38874 |
[Frege1879]
p. 63 | Proposition 78 | frege78 39070 |
[Frege1879]
p. 63 | Proposition 79 | frege79 39071 |
[Frege1879]
p. 63 | Proposition 80 | frege80 39072 |
[Frege1879]
p. 63 | Proposition 81 | frege81 39073 frege81d 38875 |
[Frege1879]
p. 64 | Proposition 82 | frege82 39074 |
[Frege1879]
p. 65 | Proposition 83 | frege83 39075 frege83d 38876 |
[Frege1879]
p. 65 | Proposition 84 | frege84 39076 |
[Frege1879]
p. 66 | Proposition 85 | frege85 39077 |
[Frege1879]
p. 66 | Proposition 86 | frege86 39078 |
[Frege1879]
p. 66 | Proposition 87 | frege87 39079 frege87d 38878 |
[Frege1879]
p. 67 | Proposition 88 | frege88 39080 |
[Frege1879]
p. 68 | Proposition 89 | frege89 39081 |
[Frege1879]
p. 68 | Proposition 90 | frege90 39082 |
[Frege1879]
p. 68 | Proposition 91 | frege91 39083 frege91d 38879 |
[Frege1879]
p. 69 | Proposition 92 | frege92 39084 |
[Frege1879]
p. 70 | Proposition 93 | frege93 39085 |
[Frege1879]
p. 70 | Proposition 94 | frege94 39086 |
[Frege1879]
p. 70 | Proposition 95 | frege95 39087 |
[Frege1879]
p. 71 | Definition 99 | dffrege99 39091 |
[Frege1879]
p. 71 | Proposition 96 | frege96 39088 frege96d 38877 |
[Frege1879]
p. 71 | Proposition 97 | frege97 39089 frege97d 38880 |
[Frege1879]
p. 71 | Proposition 98 | frege98 39090 frege98d 38881 |
[Frege1879]
p. 72 | Proposition 100 | frege100 39092 |
[Frege1879]
p. 72 | Proposition 101 | frege101 39093 |
[Frege1879]
p. 72 | Proposition 102 | frege102 39094 frege102d 38882 |
[Frege1879]
p. 73 | Proposition 103 | frege103 39095 |
[Frege1879]
p. 73 | Proposition 104 | frege104 39096 |
[Frege1879]
p. 73 | Proposition 105 | frege105 39097 |
[Frege1879]
p. 73 | Proposition 106 | frege106 39098 frege106d 38883 |
[Frege1879]
p. 74 | Proposition 107 | frege107 39099 |
[Frege1879]
p. 74 | Proposition 108 | frege108 39100 frege108d 38884 |
[Frege1879]
p. 74 | Proposition 109 | frege109 39101 frege109d 38885 |
[Frege1879]
p. 75 | Proposition 110 | frege110 39102 |
[Frege1879]
p. 75 | Proposition 111 | frege111 39103 frege111d 38887 |
[Frege1879]
p. 76 | Proposition 112 | frege112 39104 |
[Frege1879]
p. 76 | Proposition 113 | frege113 39105 |
[Frege1879]
p. 76 | Proposition 114 | frege114 39106 frege114d 38886 |
[Frege1879]
p. 77 | Definition 115 | dffrege115 39107 |
[Frege1879]
p. 77 | Proposition 116 | frege116 39108 |
[Frege1879]
p. 78 | Proposition 117 | frege117 39109 |
[Frege1879]
p. 78 | Proposition 118 | frege118 39110 |
[Frege1879]
p. 78 | Proposition 119 | frege119 39111 |
[Frege1879]
p. 78 | Proposition 120 | frege120 39112 |
[Frege1879]
p. 79 | Proposition 121 | frege121 39113 |
[Frege1879]
p. 79 | Proposition 122 | frege122 39114 frege122d 38888 |
[Frege1879]
p. 79 | Proposition 123 | frege123 39115 |
[Frege1879]
p. 80 | Proposition 124 | frege124 39116 frege124d 38889 |
[Frege1879]
p. 81 | Proposition 125 | frege125 39117 |
[Frege1879]
p. 81 | Proposition 126 | frege126 39118 frege126d 38890 |
[Frege1879]
p. 82 | Proposition 127 | frege127 39119 |
[Frege1879]
p. 83 | Proposition 128 | frege128 39120 |
[Frege1879]
p. 83 | Proposition 129 | frege129 39121 frege129d 38891 |
[Frege1879]
p. 84 | Proposition 130 | frege130 39122 |
[Frege1879]
p. 85 | Proposition 131 | frege131 39123 frege131d 38892 |
[Frege1879]
p. 86 | Proposition 132 | frege132 39124 |
[Frege1879]
p. 86 | Proposition 133 | frege133 39125 frege133d 38893 |
[Fremlin1]
p. 13 | Definition 111G (b) | df-salgen 41318 |
[Fremlin1]
p. 13 | Definition 111G (d) | borelmbl 41638 |
[Fremlin1]
p. 13 | Proposition 111G (b) | salgenss 41339 |
[Fremlin1]
p. 14 | Definition 112A | ismea 41453 |
[Fremlin1]
p. 15 | Remark 112B (d) | psmeasure 41473 |
[Fremlin1]
p. 15 | Property 112C (a) | meadjun 41464 meadjunre 41478 |
[Fremlin1]
p. 15 | Property 112C (b) | meassle 41465 |
[Fremlin1]
p. 15 | Property 112C (c) | meaunle 41466 |
[Fremlin1]
p. 16 | Property 112C (d) | iundjiun 41462 meaiunle 41471 meaiunlelem 41470 |
[Fremlin1]
p. 16 | Proposition 112C (e) | meaiuninc 41483 meaiuninc2 41484 meaiuninc3 41487 meaiuninc3v 41486 meaiunincf 41485 meaiuninclem 41482 |
[Fremlin1]
p. 16 | Proposition 112C (f) | meaiininc 41489 meaiininc2 41490 meaiininclem 41488 |
[Fremlin1]
p. 19 | Theorem 113C | caragen0 41508 caragendifcl 41516 caratheodory 41530 omelesplit 41520 |
[Fremlin1]
p. 19 | Definition 113A | isome 41496 isomennd 41533 isomenndlem 41532 |
[Fremlin1]
p. 19 | Remark 113B (c) | omeunle 41518 |
[Fremlin1]
p. 19 | Definition 112Df | caragencmpl 41537 voncmpl 41623 |
[Fremlin1]
p. 19 | Definition 113A (ii) | omessle 41500 |
[Fremlin1]
p. 20 | Theorem 113C | carageniuncl 41525 carageniuncllem1 41523 carageniuncllem2 41524 caragenuncl 41515 caragenuncllem 41514 caragenunicl 41526 |
[Fremlin1]
p. 21 | Remark 113D | caragenel2d 41534 |
[Fremlin1]
p. 21 | Theorem 113C | caratheodorylem1 41528 caratheodorylem2 41529 |
[Fremlin1]
p. 21 | Exercise 113Xa | caragencmpl 41537 |
[Fremlin1]
p. 23 | Lemma 114B | hoidmv1le 41596 hoidmv1lelem1 41593 hoidmv1lelem2 41594 hoidmv1lelem3 41595 |
[Fremlin1]
p. 25 | Definition 114E | isvonmbl 41640 |
[Fremlin1]
p. 29 | Lemma 115B | hoidmv1le 41596 hoidmvle 41602 hoidmvlelem1 41597 hoidmvlelem2 41598 hoidmvlelem3 41599 hoidmvlelem4 41600 hoidmvlelem5 41601 hsphoidmvle2 41587 hsphoif 41578 hsphoival 41581 |
[Fremlin1]
p. 29 | Definition 1135 (b) | hoicvr 41550 |
[Fremlin1]
p. 29 | Definition 115A (b) | hoicvrrex 41558 |
[Fremlin1]
p. 29 | Definition 115A (c) | hoidmv0val 41585 hoidmvn0val 41586 hoidmvval 41579 hoidmvval0 41589 hoidmvval0b 41592 |
[Fremlin1]
p. 30 | Lemma 115B | hoiprodp1 41590 hsphoidmvle 41588 |
[Fremlin1]
p. 30 | Definition 115C | df-ovoln 41539 df-voln 41541 |
[Fremlin1]
p. 30 | Proposition 115D (a) | dmovn 41606 ovn0 41568 ovn0lem 41567 ovnf 41565 ovnome 41575 ovnssle 41563 ovnsslelem 41562 ovnsupge0 41559 |
[Fremlin1]
p. 30 | Proposition 115D (b) | ovnhoi 41605 ovnhoilem1 41603 ovnhoilem2 41604 vonhoi 41669 |
[Fremlin1]
p. 31 | Lemma 115F | hoidifhspdmvle 41622 hoidifhspf 41620 hoidifhspval 41610 hoidifhspval2 41617 hoidifhspval3 41621 hspmbl 41631 hspmbllem1 41628 hspmbllem2 41629 hspmbllem3 41630 |
[Fremlin1]
p. 31 | Definition 115E | voncmpl 41623 vonmea 41576 |
[Fremlin1]
p. 31 | Proposition 115D (a)(iv) | ovnsubadd 41574 ovnsubadd2 41648 ovnsubadd2lem 41647 ovnsubaddlem1 41572 ovnsubaddlem2 41573 |
[Fremlin1]
p. 32 | Proposition 115G (a) | hoimbl 41633 hoimbl2 41667 hoimbllem 41632 hspdifhsp 41618 opnvonmbl 41636 opnvonmbllem2 41635 |
[Fremlin1]
p. 32 | Proposition 115G (b) | borelmbl 41638 |
[Fremlin1]
p. 32 | Proposition 115G (c) | iccvonmbl 41681 iccvonmbllem 41680 ioovonmbl 41679 |
[Fremlin1]
p. 32 | Proposition 115G (d) | vonicc 41687 vonicclem2 41686 vonioo 41684 vonioolem2 41683 vonn0icc 41690 vonn0icc2 41694 vonn0ioo 41689 vonn0ioo2 41692 |
[Fremlin1]
p. 32 | Proposition 115G (e) | ctvonmbl 41691 snvonmbl 41688 vonct 41695 vonsn 41693 |
[Fremlin1]
p. 35 | Lemma 121A | subsalsal 41362 |
[Fremlin1]
p. 35 | Lemma 121A (iii) | subsaliuncl 41361 subsaliuncllem 41360 |
[Fremlin1]
p. 35 | Proposition 121B | salpreimagtge 41722 salpreimalegt 41708 salpreimaltle 41723 |
[Fremlin1]
p. 35 | Proposition 121B (i) | issmf 41725 issmff 41731 issmflem 41724 |
[Fremlin1]
p. 35 | Proposition 121B (ii) | issmfle 41742 issmflelem 41741 smfpreimale 41751 |
[Fremlin1]
p. 35 | Proposition 121B (iii) | issmfgt 41753 issmfgtlem 41752 |
[Fremlin1]
p. 36 | Definition 121C | df-smblfn 41698 issmf 41725 issmff 41731 issmfge 41766 issmfgelem 41765 issmfgt 41753 issmfgtlem 41752 issmfle 41742 issmflelem 41741 issmflem 41724 |
[Fremlin1]
p. 36 | Proposition 121B | salpreimagelt 41706 salpreimagtlt 41727 salpreimalelt 41726 |
[Fremlin1]
p. 36 | Proposition 121B (iv) | issmfge 41766 issmfgelem 41765 |
[Fremlin1]
p. 36 | Proposition 121D (a) | bormflebmf 41750 |
[Fremlin1]
p. 36 | Proposition 121D (b) | cnfrrnsmf 41748 cnfsmf 41737 |
[Fremlin1]
p. 36 | Proposition 121D (c) | decsmf 41763 decsmflem 41762 incsmf 41739 incsmflem 41738 |
[Fremlin1]
p. 37 | Proposition 121E (a) | pimconstlt0 41702 pimconstlt1 41703 smfconst 41746 |
[Fremlin1]
p. 37 | Proposition 121E (b) | smfadd 41761 smfaddlem1 41759 smfaddlem2 41760 |
[Fremlin1]
p. 37 | Proposition 121E (c) | smfmulc1 41791 |
[Fremlin1]
p. 37 | Proposition 121E (d) | smfmul 41790 smfmullem1 41786 smfmullem2 41787 smfmullem3 41788 smfmullem4 41789 |
[Fremlin1]
p. 37 | Proposition 121E (e) | smfdiv 41792 |
[Fremlin1]
p. 37 | Proposition 121E (f) | smfpimbor1 41795 smfpimbor1lem2 41794 |
[Fremlin1]
p. 37 | Proposition 121E (g) | smfco 41797 |
[Fremlin1]
p. 37 | Proposition 121E (h) | smfres 41785 |
[Fremlin1]
p. 38 | Proposition 121E (e) | smfrec 41784 |
[Fremlin1]
p. 38 | Proposition 121E (f) | smfpimbor1lem1 41793 smfresal 41783 |
[Fremlin1]
p. 38 | Proposition 121F (a) | smflim 41773 smflim2 41800 smflimlem1 41767 smflimlem2 41768 smflimlem3 41769 smflimlem4 41770 smflimlem5 41771 smflimlem6 41772 smflimmpt 41804 |
[Fremlin1]
p. 38 | Proposition 121F (b) | smfsup 41808 smfsuplem1 41805 smfsuplem2 41806 smfsuplem3 41807 smfsupmpt 41809 smfsupxr 41810 |
[Fremlin1]
p. 38 | Proposition 121F (c) | smfinf 41812 smfinflem 41811 smfinfmpt 41813 |
[Fremlin1]
p. 39 | Remark 121G | smflim 41773 smflim2 41800 smflimmpt 41804 |
[Fremlin1]
p. 39 | Proposition 121F | smfpimcc 41802 |
[Fremlin1]
p. 39 | Proposition 121F (d) | smflimsup 41822 smflimsuplem2 41815 smflimsuplem6 41819 smflimsuplem7 41820 smflimsuplem8 41821 smflimsupmpt 41823 |
[Fremlin1]
p. 39 | Proposition 121F (e) | smfliminf 41825 smfliminflem 41824 smfliminfmpt 41826 |
[Fremlin1]
p. 80 | Definition 135E (b) | df-smblfn 41698 |
[Fremlin5] p.
193 | Proposition 563Gb | nulmbl2 23709 |
[Fremlin5] p.
213 | Lemma 565Ca | uniioovol 23752 |
[Fremlin5] p.
214 | Lemma 565Ca | uniioombl 23762 |
[Fremlin5]
p. 218 | Lemma 565Ib | ftc1anclem6 34028 |
[Fremlin5]
p. 220 | Theorem 565Ma | ftc1anc 34031 |
[FreydScedrov] p.
283 | Axiom of Infinity | ax-inf 8819 inf1 8803
inf2 8804 |
[Gleason] p.
117 | Proposition 9-2.1 | df-enq 10055 enqer 10065 |
[Gleason] p.
117 | Proposition 9-2.2 | df-1nq 10060 df-nq 10056 |
[Gleason] p.
117 | Proposition 9-2.3 | df-plpq 10052 df-plq 10058 |
[Gleason] p.
119 | Proposition 9-2.4 | caovmo 7136 df-mpq 10053 df-mq 10059 |
[Gleason] p.
119 | Proposition 9-2.5 | df-rq 10061 |
[Gleason] p.
119 | Proposition 9-2.6 | ltexnq 10119 |
[Gleason] p.
120 | Proposition 9-2.6(i) | halfnq 10120 ltbtwnnq 10122 |
[Gleason] p.
120 | Proposition 9-2.6(ii) | ltanq 10115 |
[Gleason] p.
120 | Proposition 9-2.6(iii) | ltmnq 10116 |
[Gleason] p.
120 | Proposition 9-2.6(iv) | ltrnq 10123 |
[Gleason] p.
121 | Definition 9-3.1 | df-np 10125 |
[Gleason] p.
121 | Definition 9-3.1 (ii) | prcdnq 10137 |
[Gleason] p.
121 | Definition 9-3.1(iii) | prnmax 10139 |
[Gleason] p.
122 | Definition | df-1p 10126 |
[Gleason] p. 122 | Remark
(1) | prub 10138 |
[Gleason] p. 122 | Lemma
9-3.4 | prlem934 10177 |
[Gleason] p.
122 | Proposition 9-3.2 | df-ltp 10129 |
[Gleason] p.
122 | Proposition 9-3.3 | ltsopr 10176 psslinpr 10175 supexpr 10198 suplem1pr 10196 suplem2pr 10197 |
[Gleason] p.
123 | Proposition 9-3.5 | addclpr 10162 addclprlem1 10160 addclprlem2 10161 df-plp 10127 |
[Gleason] p.
123 | Proposition 9-3.5(i) | addasspr 10166 |
[Gleason] p.
123 | Proposition 9-3.5(ii) | addcompr 10165 |
[Gleason] p.
123 | Proposition 9-3.5(iii) | ltaddpr 10178 |
[Gleason] p.
123 | Proposition 9-3.5(iv) | ltexpri 10187 ltexprlem1 10180 ltexprlem2 10181 ltexprlem3 10182 ltexprlem4 10183 ltexprlem5 10184 ltexprlem6 10185 ltexprlem7 10186 |
[Gleason] p.
123 | Proposition 9-3.5(v) | ltapr 10189 ltaprlem 10188 |
[Gleason] p.
123 | Proposition 9-3.5(vi) | addcanpr 10190 |
[Gleason] p. 124 | Lemma
9-3.6 | prlem936 10191 |
[Gleason] p.
124 | Proposition 9-3.7 | df-mp 10128 mulclpr 10164 mulclprlem 10163 reclem2pr 10192 |
[Gleason] p.
124 | Theorem 9-3.7(iv) | 1idpr 10173 |
[Gleason] p.
124 | Proposition 9-3.7(i) | mulasspr 10168 |
[Gleason] p.
124 | Proposition 9-3.7(ii) | mulcompr 10167 |
[Gleason] p.
124 | Proposition 9-3.7(iii) | distrpr 10172 |
[Gleason] p.
124 | Proposition 9-3.7(v) | recexpr 10195 reclem3pr 10193 reclem4pr 10194 |
[Gleason] p.
126 | Proposition 9-4.1 | df-enr 10199 enrer 10207 |
[Gleason] p.
126 | Proposition 9-4.2 | df-0r 10204 df-1r 10205 df-nr 10200 |
[Gleason] p.
126 | Proposition 9-4.3 | df-mr 10202 df-plr 10201 negexsr 10246 recexsr 10251 recexsrlem 10247 |
[Gleason] p.
127 | Proposition 9-4.4 | df-ltr 10203 |
[Gleason] p.
130 | Proposition 10-1.3 | creui 11352 creur 11351 cru 11349 |
[Gleason] p.
130 | Definition 10-1.1(v) | ax-cnre 10332 axcnre 10308 |
[Gleason] p.
132 | Definition 10-3.1 | crim 14239 crimd 14356 crimi 14317 crre 14238 crred 14355 crrei 14316 |
[Gleason] p.
132 | Definition 10-3.2 | remim 14241 remimd 14322 |
[Gleason] p.
133 | Definition 10.36 | absval2 14408 absval2d 14568 absval2i 14520 |
[Gleason] p.
133 | Proposition 10-3.4(a) | cjadd 14265 cjaddd 14344 cjaddi 14312 |
[Gleason] p.
133 | Proposition 10-3.4(c) | cjmul 14266 cjmuld 14345 cjmuli 14313 |
[Gleason] p.
133 | Proposition 10-3.4(e) | cjcj 14264 cjcjd 14323 cjcji 14295 |
[Gleason] p.
133 | Proposition 10-3.4(f) | cjre 14263 cjreb 14247 cjrebd 14326 cjrebi 14298 cjred 14350 rere 14246 rereb 14244 rerebd 14325 rerebi 14297 rered 14348 |
[Gleason] p.
133 | Proposition 10-3.4(h) | addcj 14272 addcjd 14336 addcji 14307 |
[Gleason] p.
133 | Proposition 10-3.7(a) | absval 14362 |
[Gleason] p.
133 | Proposition 10-3.7(b) | abscj 14403 abscjd 14573 abscji 14524 |
[Gleason] p.
133 | Proposition 10-3.7(c) | abs00 14413 abs00d 14569 abs00i 14521 absne0d 14570 |
[Gleason] p.
133 | Proposition 10-3.7(d) | releabs 14445 releabsd 14574 releabsi 14525 |
[Gleason] p.
133 | Proposition 10-3.7(f) | absmul 14418 absmuld 14577 absmuli 14527 |
[Gleason] p.
133 | Proposition 10-3.7(g) | sqabsadd 14406 sqabsaddi 14528 |
[Gleason] p.
133 | Proposition 10-3.7(h) | abstri 14454 abstrid 14579 abstrii 14531 |
[Gleason] p.
134 | Definition 10-4.1 | 0exp0e1 13166 df-exp 13162 exp0 13165 expp1 13168 expp1d 13310 |
[Gleason] p.
135 | Proposition 10-4.2(a) | cxpadd 24831 cxpaddd 24869 expadd 13203 expaddd 13311 expaddz 13205 |
[Gleason] p.
135 | Proposition 10-4.2(b) | cxpmul 24840 cxpmuld 24888 expmul 13206 expmuld 13312 expmulz 13207 |
[Gleason] p.
135 | Proposition 10-4.2(c) | mulcxp 24837 mulcxpd 24880 mulexp 13200 mulexpd 13324 mulexpz 13201 |
[Gleason] p.
140 | Exercise 1 | znnen 15322 |
[Gleason] p.
141 | Definition 11-2.1 | fzval 12628 |
[Gleason] p.
168 | Proposition 12-2.1(a) | climadd 14746 rlimadd 14757 rlimdiv 14760 |
[Gleason] p.
168 | Proposition 12-2.1(b) | climsub 14748 rlimsub 14758 |
[Gleason] p.
168 | Proposition 12-2.1(c) | climmul 14747 rlimmul 14759 |
[Gleason] p.
171 | Corollary 12-2.2 | climmulc2 14751 |
[Gleason] p.
172 | Corollary 12-2.5 | climrecl 14698 |
[Gleason] p.
172 | Proposition 12-2.4(c) | climabs 14718 climcj 14719 climim 14721 climre 14720 rlimabs 14723 rlimcj 14724 rlimim 14726 rlimre 14725 |
[Gleason] p.
173 | Definition 12-3.1 | df-ltxr 10403 df-xr 10402 ltxr 12242 |
[Gleason] p.
175 | Definition 12-4.1 | df-limsup 14586 limsupval 14589 |
[Gleason] p.
180 | Theorem 12-5.1 | climsup 14784 |
[Gleason] p.
180 | Theorem 12-5.3 | caucvg 14793 caucvgb 14794 caucvgr 14790 climcau 14785 |
[Gleason] p.
182 | Exercise 3 | cvgcmp 14929 |
[Gleason] p.
182 | Exercise 4 | cvgrat 14995 |
[Gleason] p.
195 | Theorem 13-2.12 | abs1m 14459 |
[Gleason] p. 217 | Lemma
13-4.1 | btwnzge0 12931 |
[Gleason] p.
223 | Definition 14-1.1 | df-met 20107 |
[Gleason] p.
223 | Definition 14-1.1(a) | met0 22525 xmet0 22524 |
[Gleason] p.
223 | Definition 14-1.1(b) | metgt0 22541 |
[Gleason] p.
223 | Definition 14-1.1(c) | metsym 22532 |
[Gleason] p.
223 | Definition 14-1.1(d) | mettri 22534 mstri 22651 xmettri 22533 xmstri 22650 |
[Gleason] p.
225 | Definition 14-1.5 | xpsmet 22564 |
[Gleason] p.
230 | Proposition 14-2.6 | txlm 21829 |
[Gleason] p.
240 | Theorem 14-4.3 | metcnp4 23485 |
[Gleason] p.
240 | Proposition 14-4.2 | metcnp3 22722 |
[Gleason] p.
243 | Proposition 14-4.16 | addcn 23045 addcn2 14708 mulcn 23047 mulcn2 14710 subcn 23046 subcn2 14709 |
[Gleason] p.
295 | Remark | bcval3 13393 bcval4 13394 |
[Gleason] p.
295 | Equation 2 | bcpasc 13408 |
[Gleason] p.
295 | Definition of binomial coefficient | bcval 13391 df-bc 13390 |
[Gleason] p.
296 | Remark | bcn0 13397 bcnn 13399 |
[Gleason] p.
296 | Theorem 15-2.8 | binom 14943 |
[Gleason] p.
308 | Equation 2 | ef0 15200 |
[Gleason] p.
308 | Equation 3 | efcj 15201 |
[Gleason] p.
309 | Corollary 15-4.3 | efne0 15206 |
[Gleason] p.
309 | Corollary 15-4.4 | efexp 15210 |
[Gleason] p.
310 | Equation 14 | sinadd 15273 |
[Gleason] p.
310 | Equation 15 | cosadd 15274 |
[Gleason] p.
311 | Equation 17 | sincossq 15285 |
[Gleason] p.
311 | Equation 18 | cosbnd 15290 sinbnd 15289 |
[Gleason] p. 311 | Lemma
15-4.7 | sqeqor 13279 sqeqori 13277 |
[Gleason] p.
311 | Definition of ` ` | df-pi 15182 |
[Godowski]
p. 730 | Equation SF | goeqi 29683 |
[GodowskiGreechie] p.
249 | Equation IV | 3oai 29078 |
[Golan] p.
1 | Remark | srgisid 18889 |
[Golan] p.
1 | Definition | df-srg 18867 |
[Golan] p.
149 | Definition | df-slmd 30295 |
[GramKnuthPat], p. 47 | Definition
2.42 | df-fwddif 32800 |
[Gratzer] p. 23 | Section
0.6 | df-mre 16606 |
[Gratzer] p. 27 | Section
0.6 | df-mri 16608 |
[Hall] p.
1 | Section 1.1 | df-asslaw 42685 df-cllaw 42683 df-comlaw 42684 |
[Hall] p.
2 | Section 1.2 | df-clintop 42697 |
[Hall] p.
7 | Section 1.3 | df-sgrp2 42718 |
[Halmos] p.
31 | Theorem 17.3 | riesz1 29475 riesz2 29476 |
[Halmos] p.
41 | Definition of Hermitian | hmopadj2 29351 |
[Halmos] p.
42 | Definition of projector ordering | pjordi 29583 |
[Halmos] p.
43 | Theorem 26.1 | elpjhmop 29595 elpjidm 29594 pjnmopi 29558 |
[Halmos] p.
44 | Remark | pjinormi 29097 pjinormii 29086 |
[Halmos] p.
44 | Theorem 26.2 | elpjch 29599 pjrn 29117 pjrni 29112 pjvec 29106 |
[Halmos] p.
44 | Theorem 26.3 | pjnorm2 29137 |
[Halmos] p.
44 | Theorem 26.4 | hmopidmpj 29564 hmopidmpji 29562 |
[Halmos] p.
45 | Theorem 27.1 | pjinvari 29601 |
[Halmos] p.
45 | Theorem 27.3 | pjoci 29590 pjocvec 29107 |
[Halmos] p.
45 | Theorem 27.4 | pjorthcoi 29579 |
[Halmos] p.
48 | Theorem 29.2 | pjssposi 29582 |
[Halmos] p.
48 | Theorem 29.3 | pjssdif1i 29585 pjssdif2i 29584 |
[Halmos] p.
50 | Definition of spectrum | df-spec 29265 |
[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 1894 |
[Hatcher] p.
25 | Definition | df-phtpc 23168 df-phtpy 23147 |
[Hatcher] p.
26 | Definition | df-pco 23181 df-pi1 23184 |
[Hatcher] p.
26 | Proposition 1.2 | phtpcer 23171 |
[Hatcher] p.
26 | Proposition 1.3 | pi1grp 23226 |
[Hefferon] p.
240 | Definition 3.12 | df-dmat 20671 df-dmatalt 43048 |
[Helfgott]
p. 2 | Theorem | tgoldbach 42549 |
[Helfgott]
p. 4 | Corollary 1.1 | wtgoldbnnsum4prm 42534 |
[Helfgott]
p. 4 | Section 1.2.2 | ax-hgprmladder 42546 bgoldbtbnd 42541 bgoldbtbnd 42541 tgblthelfgott 42547 |
[Helfgott]
p. 5 | Proposition 1.1 | circlevma 31265 |
[Helfgott]
p. 69 | Statement 7.49 | circlemethhgt 31266 |
[Helfgott]
p. 69 | Statement 7.50 | hgt750lema 31280 hgt750lemb 31279 hgt750leme 31281 hgt750lemf 31276 hgt750lemg 31277 |
[Helfgott]
p. 70 | Section 7.4 | ax-tgoldbachgt 42543 tgoldbachgt 31286 tgoldbachgtALTV 42544 tgoldbachgtd 31285 |
[Helfgott]
p. 70 | Statement 7.49 | ax-hgt749 31267 |
[Herstein] p.
54 | Exercise 28 | df-grpo 27899 |
[Herstein] p. 55 | Lemma
2.2.1(a) | grpideu 17794 grpoideu 27915 mndideu 17664 |
[Herstein] p. 55 | Lemma
2.2.1(b) | grpinveu 17817 grpoinveu 27925 |
[Herstein] p. 55 | Lemma
2.2.1(c) | grpinvinv 17843 grpo2inv 27937 |
[Herstein] p. 55 | Lemma
2.2.1(d) | grpinvadd 17854 grpoinvop 27939 |
[Herstein] p.
57 | Exercise 1 | dfgrp3e 17876 |
[Hitchcock] p. 5 | Rule
A3 | mptnan 1867 |
[Hitchcock] p. 5 | Rule
A4 | mptxor 1868 |
[Hitchcock] p. 5 | Rule
A5 | mtpxor 1870 |
[Holland] p.
1519 | Theorem 2 | sumdmdi 29830 |
[Holland] p.
1520 | Lemma 5 | cdj1i 29843 cdj3i 29851 cdj3lem1 29844 cdjreui 29842 |
[Holland] p.
1524 | Lemma 7 | mddmdin0i 29841 |
[Holland95]
p. 13 | Theorem 3.6 | hlathil 38031 |
[Holland95]
p. 14 | Line 15 | hgmapvs 37961 |
[Holland95]
p. 14 | Line 16 | hdmaplkr 37983 |
[Holland95]
p. 14 | Line 17 | hdmapellkr 37984 |
[Holland95]
p. 14 | Line 19 | hdmapglnm2 37981 |
[Holland95]
p. 14 | Line 20 | hdmapip0com 37987 |
[Holland95]
p. 14 | Theorem 3.6 | hdmapevec2 37906 |
[Holland95]
p. 14 | Lines 24 and 25 | hdmapoc 38001 |
[Holland95] p.
204 | Definition of involution | df-srng 19209 |
[Holland95]
p. 212 | Definition of subspace | df-psubsp 35573 |
[Holland95]
p. 214 | Lemma 3.3 | lclkrlem2v 37598 |
[Holland95]
p. 214 | Definition 3.2 | df-lpolN 37551 |
[Holland95]
p. 214 | Definition of nonsingular | pnonsingN 36003 |
[Holland95]
p. 215 | Lemma 3.3(1) | dihoml4 37447 poml4N 36023 |
[Holland95]
p. 215 | Lemma 3.3(2) | dochexmid 37538 pexmidALTN 36048 pexmidN 36039 |
[Holland95]
p. 218 | Theorem 3.6 | lclkr 37603 |
[Holland95]
p. 218 | Definition of dual vector space | df-ldual 35194 ldualset 35195 |
[Holland95]
p. 222 | Item 1 | df-lines 35571 df-pointsN 35572 |
[Holland95]
p. 222 | Item 2 | df-polarityN 35973 |
[Holland95]
p. 223 | Remark | ispsubcl2N 36017 omllaw4 35316 pol1N 35980 polcon3N 35987 |
[Holland95]
p. 223 | Definition | df-psubclN 36005 |
[Holland95]
p. 223 | Equation for polarity | polval2N 35976 |
[Holmes] p.
40 | Definition | df-xrn 34676 |
[Hughes] p.
44 | Equation 1.21b | ax-his3 28492 |
[Hughes] p.
47 | Definition of projection operator | dfpjop 29592 |
[Hughes] p.
49 | Equation 1.30 | eighmre 29373 eigre 29245 eigrei 29244 |
[Hughes] p.
49 | Equation 1.31 | eighmorth 29374 eigorth 29248 eigorthi 29247 |
[Hughes] p.
137 | Remark (ii) | eigposi 29246 |
[Huneke] p. 1 | Claim
1 | frgrncvvdeq 27686 |
[Huneke] p. 1 | Statement
1 | frgrncvvdeqlem7 27682 |
[Huneke] p. 1 | Statement
2 | frgrncvvdeqlem8 27683 |
[Huneke] p. 1 | Statement
3 | frgrncvvdeqlem9 27684 |
[Huneke] p. 2 | Claim
2 | frgrregorufr 27702 frgrregorufr0 27701 frgrregorufrg 27703 |
[Huneke] p. 2 | Claim
3 | frgrhash2wsp 27709 frrusgrord 27718 frrusgrord0 27717 |
[Huneke] p.
2 | Statement | df-clwwlknon 27459 |
[Huneke] p. 2 | Statement
4 | frgrwopreglem4 27692 |
[Huneke] p. 2 | Statement
5 | frgrwopreg1 27695 frgrwopreg2 27696 frgrwopregasn 27693 frgrwopregbsn 27694 |
[Huneke] p. 2 | Statement
6 | frgrwopreglem5 27698 |
[Huneke] p. 2 | Statement
7 | fusgreghash2wspv 27712 |
[Huneke] p. 2 | Statement
8 | fusgreghash2wsp 27715 |
[Huneke] p. 2 | Statement
9 | clwlksndivn 27457 numclwlk1 27770 numclwlk1lem1 27768 numclwlk1lem2 27769 numclwwlk1 27755 numclwwlk8 27803 |
[Huneke] p. 2 | Definition
3 | frgrwopreglem1 27689 |
[Huneke] p. 2 | Definition
4 | df-clwlks 27080 |
[Huneke] p. 2 | Definition
6 | 2clwwlk 27727 |
[Huneke] p. 2 | Definition
7 | numclwwlkovh 27772 numclwwlkovh0 27771 |
[Huneke] p. 2 | Statement
10 | numclwwlk2 27784 |
[Huneke] p. 2 | Statement
11 | rusgrnumwlkg 27314 |
[Huneke] p. 2 | Statement
12 | numclwwlk3 27796 |
[Huneke] p. 2 | Statement
13 | numclwwlk5 27799 |
[Huneke] p. 2 | Statement
14 | numclwwlk7 27802 |
[Indrzejczak] p.
33 | Definition ` `E | natded 27814 natded 27814 |
[Indrzejczak] p.
33 | Definition ` `I | natded 27814 |
[Indrzejczak] p.
34 | Definition ` `E | natded 27814 natded 27814 |
[Indrzejczak] p.
34 | Definition ` `I | natded 27814 |
[Jech] p. 4 | Definition of
class | cv 1655 cvjust 2820 |
[Jech] p. 42 | Lemma
6.1 | alephexp1 9723 |
[Jech] p. 42 | Equation
6.1 | alephadd 9721 alephmul 9722 |
[Jech] p. 43 | Lemma
6.2 | infmap 9720 infmap2 9362 |
[Jech] p. 71 | Lemma
9.3 | jech9.3 8961 |
[Jech] p. 72 | Equation
9.3 | scott0 9033 scottex 9032 |
[Jech] p. 72 | Exercise
9.1 | rankval4 9014 |
[Jech] p. 72 | Scheme
"Collection Principle" | cp 9038 |
[Jech] p.
78 | Note | opthprc 5404 |
[JonesMatijasevic] p.
694 | Definition 2.3 | rmxyval 38318 |
[JonesMatijasevic] p. 695 | Lemma
2.15 | jm2.15nn0 38408 |
[JonesMatijasevic] p. 695 | Lemma
2.16 | jm2.16nn0 38409 |
[JonesMatijasevic] p.
695 | Equation 2.7 | rmxadd 38330 |
[JonesMatijasevic] p.
695 | Equation 2.8 | rmyadd 38334 |
[JonesMatijasevic] p.
695 | Equation 2.9 | rmxp1 38335 rmyp1 38336 |
[JonesMatijasevic] p.
695 | Equation 2.10 | rmxm1 38337 rmym1 38338 |
[JonesMatijasevic] p.
695 | Equation 2.11 | rmx0 38328 rmx1 38329 rmxluc 38339 |
[JonesMatijasevic] p.
695 | Equation 2.12 | rmy0 38332 rmy1 38333 rmyluc 38340 |
[JonesMatijasevic] p.
695 | Equation 2.13 | rmxdbl 38342 |
[JonesMatijasevic] p.
695 | Equation 2.14 | rmydbl 38343 |
[JonesMatijasevic] p. 696 | Lemma
2.17 | jm2.17a 38365 jm2.17b 38366 jm2.17c 38367 |
[JonesMatijasevic] p. 696 | Lemma
2.19 | jm2.19 38398 |
[JonesMatijasevic] p. 696 | Lemma
2.20 | jm2.20nn 38402 |
[JonesMatijasevic] p.
696 | Theorem 2.18 | jm2.18 38393 |
[JonesMatijasevic] p. 697 | Lemma
2.24 | jm2.24 38368 jm2.24nn 38364 |
[JonesMatijasevic] p. 697 | Lemma
2.26 | jm2.26 38407 |
[JonesMatijasevic] p. 697 | Lemma
2.27 | jm2.27 38413 rmygeid 38369 |
[JonesMatijasevic] p. 698 | Lemma
3.1 | jm3.1 38425 |
[Juillerat]
p. 11 | Section *5 | etransc 41288 etransclem47 41286 etransclem48 41287 |
[Juillerat]
p. 12 | Equation (7) | etransclem44 41283 |
[Juillerat]
p. 12 | Equation *(7) | etransclem46 41285 |
[Juillerat]
p. 12 | Proof of the derivative calculated | etransclem32 41271 |
[Juillerat]
p. 13 | Proof | etransclem35 41274 |
[Juillerat]
p. 13 | Part of case 2 proven in | etransclem38 41277 |
[Juillerat]
p. 13 | Part of case 2 proven | etransclem24 41263 |
[Juillerat]
p. 13 | Part of case 2: proven in | etransclem41 41280 |
[Juillerat]
p. 14 | Proof | etransclem23 41262 |
[KalishMontague] p.
81 | Note 1 | ax-6 2075 |
[KalishMontague] p.
85 | Lemma 2 | equid 2116 |
[KalishMontague] p.
85 | Lemma 3 | equcomi 2121 |
[KalishMontague] p.
86 | Lemma 7 | cbvalivw 2111 cbvaliw 2110 wl-cbvmotv 33836 wl-motae 33838 wl-moteq 33837 |
[KalishMontague] p.
87 | Lemma 8 | spimvw 2103 spimw 2102 |
[KalishMontague] p.
87 | Lemma 9 | spfw 2140 spw 2141 |
[Kalmbach]
p. 14 | Definition of lattice | chabs1 28926 chabs1i 28928 chabs2 28927 chabs2i 28929 chjass 28943 chjassi 28896 latabs1 17447 latabs2 17448 |
[Kalmbach]
p. 15 | Definition of atom | df-at 29748 ela 29749 |
[Kalmbach]
p. 15 | Definition of covers | cvbr2 29693 cvrval2 35344 |
[Kalmbach]
p. 16 | Definition | df-ol 35248 df-oml 35249 |
[Kalmbach]
p. 20 | Definition of commutes | cmbr 28994 cmbri 29000 cmtvalN 35281 df-cm 28993 df-cmtN 35247 |
[Kalmbach]
p. 22 | Remark | omllaw5N 35317 pjoml5 29023 pjoml5i 28998 |
[Kalmbach]
p. 22 | Definition | pjoml2 29021 pjoml2i 28995 |
[Kalmbach]
p. 22 | Theorem 2(v) | cmcm 29024 cmcmi 29002 cmcmii 29007 cmtcomN 35319 |
[Kalmbach]
p. 22 | Theorem 2(ii) | omllaw3 35315 omlsi 28814 pjoml 28846 pjomli 28845 |
[Kalmbach]
p. 22 | Definition of OML law | omllaw2N 35314 |
[Kalmbach]
p. 23 | Remark | cmbr2i 29006 cmcm3 29025 cmcm3i 29004 cmcm3ii 29009 cmcm4i 29005 cmt3N 35321 cmt4N 35322 cmtbr2N 35323 |
[Kalmbach]
p. 23 | Lemma 3 | cmbr3 29018 cmbr3i 29010 cmtbr3N 35324 |
[Kalmbach]
p. 25 | Theorem 5 | fh1 29028 fh1i 29031 fh2 29029 fh2i 29032 omlfh1N 35328 |
[Kalmbach]
p. 65 | Remark | chjatom 29767 chslej 28908 chsleji 28868 shslej 28790 shsleji 28780 |
[Kalmbach]
p. 65 | Proposition 1 | chocin 28905 chocini 28864 chsupcl 28750 chsupval2 28820 h0elch 28663 helch 28651 hsupval2 28819 ocin 28706 ococss 28703 shococss 28704 |
[Kalmbach]
p. 65 | Definition of subspace sum | shsval 28722 |
[Kalmbach]
p. 66 | Remark | df-pjh 28805 pjssmi 29575 pjssmii 29091 |
[Kalmbach]
p. 67 | Lemma 3 | osum 29055 osumi 29052 |
[Kalmbach]
p. 67 | Lemma 4 | pjci 29610 |
[Kalmbach]
p. 103 | Exercise 6 | atmd2 29810 |
[Kalmbach]
p. 103 | Exercise 12 | mdsl0 29720 |
[Kalmbach]
p. 140 | Remark | hatomic 29770 hatomici 29769 hatomistici 29772 |
[Kalmbach]
p. 140 | Proposition 1 | atlatmstc 35389 |
[Kalmbach]
p. 140 | Proposition 1(i) | atexch 29791 lsatexch 35113 |
[Kalmbach]
p. 140 | Proposition 1(ii) | chcv1 29765 cvlcvr1 35409 cvr1 35480 |
[Kalmbach]
p. 140 | Proposition 1(iii) | cvexch 29784 cvexchi 29779 cvrexch 35490 |
[Kalmbach]
p. 149 | Remark 2 | chrelati 29774 hlrelat 35472 hlrelat5N 35471 lrelat 35084 |
[Kalmbach] p.
153 | Exercise 5 | lsmcv 19508 lsmsatcv 35080 spansncv 29063 spansncvi 29062 |
[Kalmbach]
p. 153 | Proposition 1(ii) | lsmcv2 35099 spansncv2 29703 |
[Kalmbach]
p. 266 | Definition | df-st 29621 |
[Kalmbach2]
p. 8 | Definition of adjoint | df-adjh 29259 |
[KanamoriPincus] p.
415 | Theorem 1.1 | fpwwe 9790 fpwwe2 9787 |
[KanamoriPincus] p.
416 | Corollary 1.3 | canth4 9791 |
[KanamoriPincus] p.
417 | Corollary 1.6 | canthp1 9798 |
[KanamoriPincus] p.
417 | Corollary 1.4(a) | canthnum 9793 |
[KanamoriPincus] p.
417 | Corollary 1.4(b) | canthwe 9795 |
[KanamoriPincus] p.
418 | Proposition 1.7 | pwfseq 9808 |
[KanamoriPincus] p.
419 | Lemma 2.2 | gchcdaidm 9812 gchxpidm 9813 |
[KanamoriPincus] p.
419 | Theorem 2.1 | gchacg 9824 gchhar 9823 |
[KanamoriPincus] p.
420 | Lemma 2.3 | pwcdadom 9360 unxpwdom 8770 |
[KanamoriPincus] p.
421 | Proposition 3.1 | gchpwdom 9814 |
[Kreyszig] p.
3 | Property M1 | metcl 22514 xmetcl 22513 |
[Kreyszig] p.
4 | Property M2 | meteq0 22521 |
[Kreyszig] p.
8 | Definition 1.1-8 | dscmet 22754 |
[Kreyszig] p.
12 | Equation 5 | conjmul 11075 muleqadd 11003 |
[Kreyszig] p.
18 | Definition 1.3-2 | mopnval 22620 |
[Kreyszig] p.
19 | Remark | mopntopon 22621 |
[Kreyszig] p.
19 | Theorem T1 | mopn0 22680 mopnm 22626 |
[Kreyszig] p.
19 | Theorem T2 | unimopn 22678 |
[Kreyszig] p.
19 | Definition of neighborhood | neibl 22683 |
[Kreyszig] p.
20 | Definition 1.3-3 | metcnp2 22724 |
[Kreyszig] p.
25 | Definition 1.4-1 | lmbr 21440 lmmbr 23433 lmmbr2 23434 |
[Kreyszig] p. 26 | Lemma
1.4-2(a) | lmmo 21562 |
[Kreyszig] p.
28 | Theorem 1.4-5 | lmcau 23488 |
[Kreyszig] p.
28 | Definition 1.4-3 | iscau 23451 iscmet2 23469 |
[Kreyszig] p.
30 | Theorem 1.4-7 | cmetss 23491 |
[Kreyszig] p.
30 | Theorem 1.4-6(a) | 1stcelcls 21642 metelcls 23480 |
[Kreyszig] p.
30 | Theorem 1.4-6(b) | metcld 23481 metcld2 23482 |
[Kreyszig] p.
51 | Equation 2 | clmvneg1 23275 lmodvneg1 19269 nvinv 28045 vcm 27982 |
[Kreyszig] p.
51 | Equation 1a | clm0vs 23271 lmod0vs 19259 slmd0vs 30318 vc0 27980 |
[Kreyszig] p.
51 | Equation 1b | lmodvs0 19260 slmdvs0 30319 vcz 27981 |
[Kreyszig] p.
58 | Definition 2.2-1 | imsmet 28097 ngpmet 22784 nrmmetd 22756 |
[Kreyszig] p.
59 | Equation 1 | imsdval 28092 imsdval2 28093 ncvspds 23337 ngpds 22785 |
[Kreyszig] p.
63 | Problem 1 | nmval 22771 nvnd 28094 |
[Kreyszig] p.
64 | Problem 2 | nmeq0 22799 nmge0 22798 nvge0 28079 nvz 28075 |
[Kreyszig] p.
64 | Problem 3 | nmrtri 22805 nvabs 28078 |
[Kreyszig] p.
91 | Definition 2.7-1 | isblo3i 28207 |
[Kreyszig] p.
92 | Equation 2 | df-nmoo 28151 |
[Kreyszig] p.
97 | Theorem 2.7-9(a) | blocn 28213 blocni 28211 |
[Kreyszig] p.
97 | Theorem 2.7-9(b) | lnocni 28212 |
[Kreyszig] p.
129 | Definition 3.1-1 | cphipeq0 23380 ipeq0 20352 ipz 28125 |
[Kreyszig] p.
135 | Problem 2 | pythi 28256 |
[Kreyszig] p.
137 | Lemma 3-2.1(a) | sii 28260 |
[Kreyszig] p.
144 | Equation 4 | supcvg 14969 |
[Kreyszig] p.
144 | Theorem 3.3-1 | minvec 23611 minveco 28291 |
[Kreyszig] p.
196 | Definition 3.9-1 | df-aj 28156 |
[Kreyszig] p.
247 | Theorem 4.7-2 | bcth 23504 |
[Kreyszig] p.
249 | Theorem 4.7-3 | ubth 28280 |
[Kreyszig]
p. 470 | Definition of positive operator ordering | leop 29533 leopg 29532 |
[Kreyszig]
p. 476 | Theorem 9.4-2 | opsqrlem2 29551 |
[Kreyszig] p.
525 | Theorem 10.1-1 | htth 28326 |
[Kulpa] p.
547 | Theorem | poimir 33981 |
[Kulpa] p.
547 | Equation (1) | poimirlem32 33980 |
[Kulpa] p.
547 | Equation (2) | poimirlem31 33979 |
[Kulpa] p.
548 | Theorem | broucube 33982 |
[Kulpa] p.
548 | Equation (6) | poimirlem26 33974 |
[Kulpa] p.
548 | Equation (7) | poimirlem27 33975 |
[Kunen] p. 10 | Axiom
0 | ax6e 2402 axnul 5014 |
[Kunen] p. 11 | Axiom
3 | axnul 5014 |
[Kunen] p. 12 | Axiom
6 | zfrep6 7401 |
[Kunen] p. 24 | Definition
10.24 | mapval 8139 mapvalg 8137 |
[Kunen] p. 30 | Lemma
10.20 | fodom 9666 |
[Kunen] p. 31 | Definition
10.24 | mapex 8133 |
[Kunen] p. 95 | Definition
2.1 | df-r1 8911 |
[Kunen] p. 97 | Lemma
2.10 | r1elss 8953 r1elssi 8952 |
[Kunen] p. 107 | Exercise
4 | rankop 9005 rankopb 8999 rankuni 9010 rankxplim 9026 rankxpsuc 9029 |
[KuratowskiMostowski] p.
109 | Section. Eq. 14 | iuniin 4753 |
[Lang] p.
3 | Definition | df-mnd 17655 |
[Lang] p.
7 | Definition | dfgrp2e 17809 |
[Lang] p.
53 | Definition | df-cat 16688 |
[Lang] p.
54 | Definition | df-iso 16768 |
[Lang] p.
57 | Definition | df-inito 17000 df-termo 17001 |
[Lang] p.
58 | Example | irinitoringc 42930 |
[Lang] p.
58 | Statement | initoeu1 17020 termoeu1 17027 |
[Lang] p.
62 | Definition | df-func 16877 |
[Lang] p.
65 | Definition | df-nat 16962 |
[Lang] p.
91 | Note | df-ringc 42866 |
[Lang] p.
128 | Remark | dsmmlmod 20459 |
[Lang] p.
129 | Proof | lincscm 43080 lincscmcl 43082 lincsum 43079 lincsumcl 43081 |
[Lang] p.
129 | Statement | lincolss 43084 |
[Lang] p.
129 | Observation | dsmmfi 20452 |
[Lang] p.
147 | Definition | snlindsntor 43121 |
[Lang] p.
504 | Statement | mat1 20628 matring 20623 |
[Lang] p.
504 | Definition | df-mamu 20564 |
[Lang] p.
505 | Statement | mamuass 20582 mamutpos 20639 matassa 20624 mattposvs 20636 tposmap 20638 |
[Lang] p.
513 | Definition | mdet1 20782 mdetf 20776 |
[Lang] p. 513 | Theorem
4.4 | cramer 20874 |
[Lang] p. 514 | Proposition
4.6 | mdetleib 20768 |
[Lang] p. 514 | Proposition
4.8 | mdettpos 20792 |
[Lang] p.
515 | Definition | df-minmar1 20816 smadiadetr 20857 |
[Lang] p. 515 | Corollary
4.9 | mdetero 20791 mdetralt 20789 |
[Lang] p. 517 | Proposition
4.15 | mdetmul 20804 |
[Lang] p.
518 | Definition | df-madu 20815 |
[Lang] p. 518 | Proposition
4.16 | madulid 20826 madurid 20825 matinv 20859 |
[Lang] p. 561 | Theorem
3.1 | cayleyhamilton 21072 |
[Lang], p.
561 | Remark | chpmatply1 21014 |
[Lang], p.
561 | Definition | df-chpmat 21009 |
[LarsonHostetlerEdwards] p.
278 | Section 4.1 | dvconstbi 39368 |
[LarsonHostetlerEdwards] p.
311 | Example 1a | lhe4.4ex1a 39363 |
[LarsonHostetlerEdwards] p.
375 | Theorem 5.1 | expgrowth 39369 |
[LeBlanc] p. 277 | Rule
R2 | axnul 5014 |
[Levy] p.
338 | Axiom | df-clab 2812 df-clel 2821 df-cleq 2818 |
[Levy58] p. 2 | Definition
I | isfin1-3 9530 |
[Levy58] p. 2 | Definition
II | df-fin2 9430 |
[Levy58] p. 2 | Definition
Ia | df-fin1a 9429 |
[Levy58] p. 2 | Definition
III | df-fin3 9432 |
[Levy58] p. 3 | Definition
V | df-fin5 9433 |
[Levy58] p. 3 | Definition
IV | df-fin4 9431 |
[Levy58] p. 4 | Definition
VI | df-fin6 9434 |
[Levy58] p. 4 | Definition
VII | df-fin7 9435 |
[Levy58], p. 3 | Theorem
1 | fin1a2 9559 |
[Lipparini]
p. 3 | Lemma 2.1.1 | nosepssdm 32370 |
[Lipparini]
p. 3 | Lemma 2.1.4 | noresle 32380 |
[Lipparini]
p. 6 | Proposition 4.2 | nosupbnd1 32394 |
[Lipparini]
p. 6 | Proposition 4.3 | nosupbnd2 32396 |
[Lipparini]
p. 7 | Theorem 5.1 | noetalem2 32398 noetalem3 32399 |
[Lopez-Astorga] p.
12 | Rule 1 | mptnan 1867 |
[Lopez-Astorga] p.
12 | Rule 2 | mptxor 1868 |
[Lopez-Astorga] p.
12 | Rule 3 | mtpxor 1870 |
[Maeda] p.
167 | Theorem 1(d) to (e) | mdsymlem6 29818 |
[Maeda] p.
168 | Lemma 5 | mdsym 29822 mdsymi 29821 |
[Maeda] p.
168 | Lemma 4(i) | mdsymlem4 29816 mdsymlem6 29818 mdsymlem7 29819 |
[Maeda] p.
168 | Lemma 4(ii) | mdsymlem8 29820 |
[MaedaMaeda] p. 1 | Remark | ssdmd1 29723 ssdmd2 29724 ssmd1 29721 ssmd2 29722 |
[MaedaMaeda] p. 1 | Lemma 1.2 | mddmd2 29719 |
[MaedaMaeda] p. 1 | Definition
1.1 | df-dmd 29691 df-md 29690 mdbr 29704 |
[MaedaMaeda] p. 2 | Lemma 1.3 | mdsldmd1i 29741 mdslj1i 29729 mdslj2i 29730 mdslle1i 29727 mdslle2i 29728 mdslmd1i 29739 mdslmd2i 29740 |
[MaedaMaeda] p. 2 | Lemma 1.4 | mdsl1i 29731 mdsl2bi 29733 mdsl2i 29732 |
[MaedaMaeda] p. 2 | Lemma 1.6 | mdexchi 29745 |
[MaedaMaeda] p. 2 | Lemma
1.5.1 | mdslmd3i 29742 |
[MaedaMaeda] p. 2 | Lemma
1.5.2 | mdslmd4i 29743 |
[MaedaMaeda] p. 2 | Lemma
1.5.3 | mdsl0 29720 |
[MaedaMaeda] p. 2 | Theorem
1.3 | dmdsl3 29725 mdsl3 29726 |
[MaedaMaeda] p. 3 | Theorem
1.9.1 | csmdsymi 29744 |
[MaedaMaeda] p. 4 | Theorem
1.14 | mdcompli 29839 |
[MaedaMaeda] p. 30 | Lemma
7.2 | atlrelat1 35391 hlrelat1 35470 |
[MaedaMaeda] p. 31 | Lemma
7.5 | lcvexch 35109 |
[MaedaMaeda] p. 31 | Lemma
7.5.1 | cvmd 29746 cvmdi 29734 cvnbtwn4 29699 cvrnbtwn4 35349 |
[MaedaMaeda] p. 31 | Lemma
7.5.2 | cvdmd 29747 |
[MaedaMaeda] p. 31 | Definition
7.4 | cvlcvrp 35410 cvp 29785 cvrp 35486 lcvp 35110 |
[MaedaMaeda] p. 31 | Theorem
7.6(b) | atmd 29809 |
[MaedaMaeda] p. 31 | Theorem
7.6(c) | atdmd 29808 |
[MaedaMaeda] p. 32 | Definition
7.8 | cvlexch4N 35403 hlexch4N 35462 |
[MaedaMaeda] p. 34 | Exercise
7.1 | atabsi 29811 |
[MaedaMaeda] p. 41 | Lemma
9.2(delta) | cvrat4 35513 |
[MaedaMaeda] p. 61 | Definition
15.1 | 0psubN 35819 atpsubN 35823 df-pointsN 35572 pointpsubN 35821 |
[MaedaMaeda] p. 62 | Theorem
15.5 | df-pmap 35574 pmap11 35832 pmaple 35831 pmapsub 35838 pmapval 35827 |
[MaedaMaeda] p. 62 | Theorem
15.5.1 | pmap0 35835 pmap1N 35837 |
[MaedaMaeda] p. 62 | Theorem
15.5.2 | pmapglb 35840 pmapglb2N 35841 pmapglb2xN 35842 pmapglbx 35839 |
[MaedaMaeda] p. 63 | Equation
15.5.3 | pmapjoin 35922 |
[MaedaMaeda] p. 67 | Postulate
PS1 | ps-1 35547 |
[MaedaMaeda] p. 68 | Lemma
16.2 | df-padd 35866 paddclN 35912 paddidm 35911 |
[MaedaMaeda] p. 68 | Condition
PS2 | ps-2 35548 |
[MaedaMaeda] p. 68 | Equation
16.2.1 | paddass 35908 |
[MaedaMaeda] p. 69 | Lemma
16.4 | ps-1 35547 |
[MaedaMaeda] p. 69 | Theorem
16.4 | ps-2 35548 |
[MaedaMaeda] p.
70 | Theorem 16.9 | lsmmod 18446 lsmmod2 18447 lssats 35082 shatomici 29768 shatomistici 29771 shmodi 28800 shmodsi 28799 |
[MaedaMaeda] p. 130 | Remark
29.6 | dmdmd 29710 mdsymlem7 29819 |
[MaedaMaeda] p. 132 | Theorem
29.13(e) | pjoml6i 28999 |
[MaedaMaeda] p. 136 | Lemma
31.1.5 | shjshseli 28903 |
[MaedaMaeda] p. 139 | Remark | sumdmdii 29825 |
[Margaris] p. 40 | Rule
C | exlimiv 2029 |
[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 387 df-ex 1879 df-or 879 dfbi2 468 |
[Margaris] p.
51 | Theorem 1 | idALT 23 |
[Margaris] p.
56 | Theorem 3 | conventions 27811 |
[Margaris]
p. 59 | Section 14 | notnotrALTVD 39964 |
[Margaris] p.
60 | Theorem 8 | mth8 160 |
[Margaris]
p. 60 | Section 14 | con3ALTVD 39965 |
[Margaris]
p. 79 | Rule C | exinst01 39673 exinst11 39674 |
[Margaris] p.
89 | Theorem 19.2 | 19.2 2080 19.2g 2229 r19.2z 4284 |
[Margaris] p.
89 | Theorem 19.3 | 19.3 2243 rr19.3v 3564 |
[Margaris] p.
89 | Theorem 19.5 | alcom 2209 |
[Margaris] p.
89 | Theorem 19.6 | alex 1924 |
[Margaris] p.
89 | Theorem 19.7 | alnex 1880 |
[Margaris] p.
89 | Theorem 19.8 | 19.8a 2223 |
[Margaris] p.
89 | Theorem 19.9 | 19.9 2247 19.9h 2317 exlimd 2261 exlimdh 2321 |
[Margaris] p.
89 | Theorem 19.11 | excom 2212 excomim 2213 |
[Margaris] p.
89 | Theorem 19.12 | 19.12 2359 |
[Margaris] p.
90 | Section 19 | conventions-labels 27812 conventions-labels 27812 conventions-labels 27812 conventions-labels 27812 |
[Margaris] p.
90 | Theorem 19.14 | exnal 1925 |
[Margaris]
p. 90 | Theorem 19.15 | 2albi 39412 albi 1917 |
[Margaris] p.
90 | Theorem 19.16 | 19.16 2268 |
[Margaris] p.
90 | Theorem 19.17 | 19.17 2269 |
[Margaris]
p. 90 | Theorem 19.18 | 2exbi 39414 exbi 1946 |
[Margaris] p.
90 | Theorem 19.19 | 19.19 2272 |
[Margaris]
p. 90 | Theorem 19.20 | 2alim 39411 2alimdv 2017 alimd 2255 alimdh 1916 alimdv 2015 ax-4 1908
ralimdaa 3167 ralimdv 3172 ralimdva 3171 ralimdvva 3173 sbcimdv 3724 |
[Margaris] p.
90 | Theorem 19.21 | 19.21 2249 19.21h 2318 19.21t 2248 19.21vv 39410 alrimd 2258 alrimdd 2257 alrimdh 1964 alrimdv 2028 alrimi 2256 alrimih 1922 alrimiv 2026 alrimivv 2027 hbralrimi 3163 r19.21be 3142 r19.21bi 3141 ralrimd 3168 ralrimdv 3177 ralrimdva 3178 ralrimdvv 3182 ralrimdvva 3183 ralrimi 3166 ralrimia 40124 ralrimiv 3174 ralrimiva 3175 ralrimivv 3179 ralrimivva 3180 ralrimivvva 3181 ralrimivw 3176 |
[Margaris]
p. 90 | Theorem 19.22 | 2exim 39413 2eximdv 2018 exim 1932
eximd 2259 eximdh 1965 eximdv 2016 rexim 3216 reximd2a 3221 reximdai 3220 reximdd 40148 reximddv 3226 reximddv2 3229 reximddv3 40147 reximdv 3224 reximdv2 3222 reximdva 3225 reximdvai 3223 reximdvva 3228 reximi2 3218 |
[Margaris] p.
90 | Theorem 19.23 | 19.23 2254 19.23bi 2232 19.23h 2319 19.23t 2252 exlimdv 2032 exlimdvv 2033 exlimexi 39563 exlimiv 2029 exlimivv 2031 rexlimd3 40140 rexlimdv 3239 rexlimdv3a 3242 rexlimdva 3240 rexlimdva2 3243 rexlimdvaa 3241 rexlimdvv 3247 rexlimdvva 3248 rexlimdvw 3244 rexlimiv 3236 rexlimiva 3237 rexlimivv 3246 |
[Margaris] p.
90 | Theorem 19.24 | 19.24 2088 |
[Margaris] p.
90 | Theorem 19.25 | 19.25 1983 |
[Margaris] p.
90 | Theorem 19.26 | 19.26 1972 |
[Margaris] p.
90 | Theorem 19.27 | 19.27 2270 r19.27z 4294 r19.27zv 4295 |
[Margaris] p.
90 | Theorem 19.28 | 19.28 2271 19.28vv 39420 r19.28z 4287 r19.28zv 4290 rr19.28v 3565 |
[Margaris] p.
90 | Theorem 19.29 | 19.29 1976 r19.29d2r 3290 r19.29imd 3284 |
[Margaris] p.
90 | Theorem 19.30 | 19.30 1984 |
[Margaris] p.
90 | Theorem 19.31 | 19.31 2277 19.31vv 39418 |
[Margaris] p.
90 | Theorem 19.32 | 19.32 2276 r19.32 41987 |
[Margaris]
p. 90 | Theorem 19.33 | 19.33-2 39416 19.33 1987 |
[Margaris] p.
90 | Theorem 19.34 | 19.34 2089 |
[Margaris] p.
90 | Theorem 19.35 | 19.35 1980 |
[Margaris] p.
90 | Theorem 19.36 | 19.36 2273 19.36vv 39417 r19.36zv 4296 |
[Margaris] p.
90 | Theorem 19.37 | 19.37 2275 19.37vv 39419 r19.37zv 4291 |
[Margaris] p.
90 | Theorem 19.38 | 19.38 1937 |
[Margaris] p.
90 | Theorem 19.39 | 19.39 2087 |
[Margaris] p.
90 | Theorem 19.40 | 19.40-2 1989 19.40 1971 r19.40 3298 |
[Margaris] p.
90 | Theorem 19.41 | 19.41 2278 19.41rg 39589 |
[Margaris] p.
90 | Theorem 19.42 | 19.42 2280 |
[Margaris] p.
90 | Theorem 19.43 | 19.43 1985 |
[Margaris] p.
90 | Theorem 19.44 | 19.44 2281 r19.44zv 4293 |
[Margaris] p.
90 | Theorem 19.45 | 19.45 2282 r19.45zv 4292 |
[Margaris] p.
110 | Exercise 2(b) | eu1 2695 |
[Mayet] p.
370 | Remark | jpi 29680 largei 29677 stri 29667 |
[Mayet3] p.
9 | Definition of CH-states | df-hst 29622 ishst 29624 |
[Mayet3] p.
10 | Theorem | hstrbi 29676 hstri 29675 |
[Mayet3] p.
1223 | Theorem 4.1 | mayete3i 29138 |
[Mayet3] p.
1240 | Theorem 7.1 | mayetes3i 29139 |
[MegPav2000] p. 2344 | Theorem
3.3 | stcltrthi 29688 |
[MegPav2000] p. 2345 | Definition
3.4-1 | chintcl 28742 chsupcl 28750 |
[MegPav2000] p. 2345 | Definition
3.4-2 | hatomic 29770 |
[MegPav2000] p. 2345 | Definition
3.4-3(a) | superpos 29764 |
[MegPav2000] p. 2345 | Definition
3.4-3(b) | atexch 29791 |
[MegPav2000] p. 2366 | Figure
7 | pl42N 36053 |
[MegPav2002] p.
362 | Lemma 2.2 | latj31 17459 latj32 17457 latjass 17455 |
[Megill] p. 444 | Axiom
C5 | ax-5 2009 ax5ALT 34977 |
[Megill] p. 444 | Section
7 | conventions 27811 |
[Megill] p.
445 | Lemma L12 | aecom-o 34971 ax-c11n 34958 axc11n 2447 |
[Megill] p. 446 | Lemma
L17 | equtrr 2126 |
[Megill] p.
446 | Lemma L18 | ax6fromc10 34966 |
[Megill] p.
446 | Lemma L19 | hbnae-o 34998 hbnae 2454 |
[Megill] p. 447 | Remark
9.1 | df-sb 2068 sbid 2289
sbidd-misc 43368 sbidd 43367 |
[Megill] p. 448 | Remark
9.6 | axc14 2503 |
[Megill] p.
448 | Scheme C4' | ax-c4 34954 |
[Megill] p.
448 | Scheme C5' | ax-c5 34953 sp 2224 |
[Megill] p. 448 | Scheme
C6' | ax-11 2207 |
[Megill] p.
448 | Scheme C7' | ax-c7 34955 |
[Megill] p. 448 | Scheme
C8' | ax-7 2112 |
[Megill] p.
448 | Scheme C9' | ax-c9 34960 |
[Megill] p. 448 | Scheme
C10' | ax-6 2075 ax-c10 34956 |
[Megill] p.
448 | Scheme C11' | ax-c11 34957 |
[Megill] p. 448 | Scheme
C12' | ax-8 2166 |
[Megill] p. 448 | Scheme
C13' | ax-9 2173 |
[Megill] p.
448 | Scheme C14' | ax-c14 34961 |
[Megill] p.
448 | Scheme C15' | ax-c15 34959 |
[Megill] p.
448 | Scheme C16' | ax-c16 34962 |
[Megill] p.
448 | Theorem 9.4 | dral1-o 34974 dral1 2460 dral2-o 35000 dral2 2459 drex1 2462 drex2 2463 drsb1 2508 drsb2 2509 |
[Megill] p. 449 | Theorem
9.7 | sbcom2 2578 sbequ 2507 sbid2v 2545 |
[Megill] p.
450 | Example in Appendix | hba1-o 34967 hba1 2325 |
[Mendelson]
p. 35 | Axiom A3 | hirstL-ax3 41847 |
[Mendelson] p.
36 | Lemma 1.8 | idALT 23 |
[Mendelson] p.
69 | Axiom 4 | rspsbc 3742 rspsbca 3743 stdpc4 2483 |
[Mendelson]
p. 69 | Axiom 5 | ax-c4 34954 ra4 3749
stdpc5 2250 |
[Mendelson] p.
81 | Rule C | exlimiv 2029 |
[Mendelson] p.
95 | Axiom 6 | stdpc6 2132 |
[Mendelson] p.
95 | Axiom 7 | stdpc7 2133 |
[Mendelson] p.
225 | Axiom system NBG | ru 3661 |
[Mendelson] p.
230 | Exercise 4.8(b) | opthwiener 5202 |
[Mendelson] p.
231 | Exercise 4.10(k) | inv1 4197 |
[Mendelson] p.
231 | Exercise 4.10(l) | unv 4198 |
[Mendelson] p.
231 | Exercise 4.10(n) | dfin3 4098 |
[Mendelson] p.
231 | Exercise 4.10(o) | df-nul 4147 |
[Mendelson] p.
231 | Exercise 4.10(q) | dfin4 4099 |
[Mendelson] p.
231 | Exercise 4.10(s) | ddif 3971 |
[Mendelson] p.
231 | Definition of union | dfun3 4097 |
[Mendelson] p.
235 | Exercise 4.12(c) | univ 5142 |
[Mendelson] p.
235 | Exercise 4.12(d) | pwv 4657 |
[Mendelson] p.
235 | Exercise 4.12(j) | pwin 5246 |
[Mendelson] p.
235 | Exercise 4.12(k) | pwunss 5247 |
[Mendelson] p.
235 | Exercise 4.12(l) | pwssun 5248 |
[Mendelson] p.
235 | Exercise 4.12(n) | uniin 4682 |
[Mendelson] p.
235 | Exercise 4.12(p) | reli 5486 |
[Mendelson] p.
235 | Exercise 4.12(t) | relssdmrn 5901 |
[Mendelson] p.
244 | Proposition 4.8(g) | epweon 7248 |
[Mendelson] p.
246 | Definition of successor | df-suc 5973 |
[Mendelson] p.
250 | Exercise 4.36 | oelim2 7947 |
[Mendelson] p.
254 | Proposition 4.22(b) | xpen 8398 |
[Mendelson] p.
254 | Proposition 4.22(c) | xpsnen 8319 xpsneng 8320 |
[Mendelson] p.
254 | Proposition 4.22(d) | xpcomen 8326 xpcomeng 8327 |
[Mendelson] p.
254 | Proposition 4.22(e) | xpassen 8329 |
[Mendelson] p.
255 | Definition | brsdom 8251 |
[Mendelson] p.
255 | Exercise 4.39 | endisj 8322 |
[Mendelson] p.
255 | Exercise 4.41 | mapprc 8131 |
[Mendelson] p.
255 | Exercise 4.43 | mapsnen 8308 mapsnend 8307 |
[Mendelson] p.
255 | Exercise 4.45 | mapunen 8404 |
[Mendelson] p.
255 | Exercise 4.47 | xpmapen 8403 |
[Mendelson] p.
255 | Exercise 4.42(a) | map0e 8166 |
[Mendelson] p.
255 | Exercise 4.42(b) | map1 8311 |
[Mendelson] p.
257 | Proposition 4.24(a) | undom 8323 |
[Mendelson] p.
258 | Exercise 4.56(b) | cdaen 9317 |
[Mendelson] p.
258 | Exercise 4.56(c) | cdaassen 9326 cdacomen 9325 |
[Mendelson] p.
258 | Exercise 4.56(f) | cdadom1 9330 |
[Mendelson] p.
258 | Exercise 4.56(g) | xp2cda 9324 |
[Mendelson] p.
258 | Definition of cardinal sum | cdaval 9314 df-cda 9312 |
[Mendelson] p.
266 | Proposition 4.34(a) | oa1suc 7883 |
[Mendelson] p.
266 | Proposition 4.34(f) | oaordex 7910 |
[Mendelson] p.
275 | Proposition 4.42(d) | entri3 9703 |
[Mendelson] p.
281 | Definition | df-r1 8911 |
[Mendelson] p.
281 | Proposition 4.45 (b) to (a) | unir1 8960 |
[Mendelson] p.
287 | Axiom system MK | ru 3661 |
[MertziosUnger] p.
152 | Definition | df-frgr 27634 |
[MertziosUnger] p.
153 | Remark 1 | frgrconngr 27671 |
[MertziosUnger] p.
153 | Remark 2 | vdgn1frgrv2 27673 vdgn1frgrv3 27674 |
[MertziosUnger] p.
153 | Remark 3 | vdgfrgrgt2 27675 |
[MertziosUnger] p.
153 | Proposition 1(a) | n4cyclfrgr 27668 |
[MertziosUnger] p.
153 | Proposition 1(b) | 2pthfrgr 27661 2pthfrgrrn 27659 2pthfrgrrn2 27660 |
[Mittelstaedt] p.
9 | Definition | df-oc 28660 |
[Monk1] p.
22 | Remark | conventions 27811 |
[Monk1] p. 22 | Theorem
3.1 | conventions 27811 |
[Monk1] p. 26 | Theorem
2.8(vii) | ssin 4061 |
[Monk1] p. 33 | Theorem
3.2(i) | ssrel 5446 ssrelf 29970 |
[Monk1] p. 33 | Theorem
3.2(ii) | eqrel 5447 |
[Monk1] p. 34 | Definition
3.3 | df-opab 4938 |
[Monk1] p. 36 | Theorem
3.7(i) | coi1 5896 coi2 5897 |
[Monk1] p. 36 | Theorem
3.8(v) | dm0 5575 rn0 5614 |
[Monk1] p. 36 | Theorem
3.7(ii) | cnvi 5782 |
[Monk1] p. 37 | Theorem
3.13(i) | relxp 5364 |
[Monk1] p. 37 | Theorem
3.13(x) | dmxp 5580 rnxp 5809 |
[Monk1] p. 37 | Theorem
3.13(ii) | 0xp 5438 xp0 5797 |
[Monk1] p. 38 | Theorem
3.16(ii) | ima0 5726 |
[Monk1] p. 38 | Theorem
3.16(viii) | imai 5723 |
[Monk1] p. 39 | Theorem
3.17 | imaex 7371 imaexg 7370 |
[Monk1] p. 39 | Theorem
3.16(xi) | imassrn 5722 |
[Monk1] p. 41 | Theorem
4.3(i) | fnopfv 6605 funfvop 6583 |
[Monk1] p. 42 | Theorem
4.3(ii) | funopfvb 6489 |
[Monk1] p. 42 | Theorem
4.4(iii) | fvelima 6499 |
[Monk1] p. 43 | Theorem
4.6 | funun 6172 |
[Monk1] p. 43 | Theorem
4.8(iv) | dff13 6772 dff13f 6773 |
[Monk1] p. 46 | Theorem
4.15(v) | funex 6743 funrnex 7400 |
[Monk1] p. 50 | Definition
5.4 | fniunfv 6765 |
[Monk1] p. 52 | Theorem
5.12(ii) | op2ndb 5865 |
[Monk1] p. 52 | Theorem
5.11(viii) | ssint 4715 |
[Monk1] p. 52 | Definition
5.13 (i) | 1stval2 7450 df-1st 7433 |
[Monk1] p. 52 | Definition
5.13 (ii) | 2ndval2 7451 df-2nd 7434 |
[Monk1] p. 112 | Theorem
15.17(v) | ranksn 9001 ranksnb 8974 |
[Monk1] p. 112 | Theorem
15.17(iv) | rankuni2 9002 |
[Monk1] p. 112 | Theorem
15.17(iii) | rankun 9003 rankunb 8997 |
[Monk1] p. 113 | Theorem
15.18 | r1val3 8985 |
[Monk1] p. 113 | Definition
15.19 | df-r1 8911 r1val2 8984 |
[Monk1] p.
117 | Lemma | zorn2 9650 zorn2g 9647 |
[Monk1] p. 133 | Theorem
18.11 | cardom 9132 |
[Monk1] p. 133 | Theorem
18.12 | canth3 9705 |
[Monk1] p. 133 | Theorem
18.14 | carduni 9127 |
[Monk2] p. 105 | Axiom
C4 | ax-4 1908 |
[Monk2] p. 105 | Axiom
C7 | ax-7 2112 |
[Monk2] p. 105 | Axiom
C8 | ax-12 2220 ax-c15 34959 ax12v2 2222 |
[Monk2] p.
108 | Lemma 5 | ax-c4 34954 |
[Monk2] p. 109 | Lemma
12 | ax-11 2207 |
[Monk2] p. 109 | Lemma
15 | equvini 2476 equvinv 2134 eqvinop 5177 |
[Monk2] p. 113 | Axiom
C5-1 | ax-5 2009 ax5ALT 34977 |
[Monk2] p. 113 | Axiom
C5-2 | ax-10 2192 |
[Monk2] p. 113 | Axiom
C5-3 | ax-11 2207 |
[Monk2] p. 114 | Lemma
21 | sp 2224 |
[Monk2] p. 114 | Lemma
22 | axc4 2352 hba1-o 34967 hba1 2325 |
[Monk2] p. 114 | Lemma
23 | nfia1 2204 |
[Monk2] p. 114 | Lemma
24 | nfa2 2219 nfra2 3155 |
[Moore] p. 53 | Part
I | df-mre 16606 |
[Munkres] p. 77 | Example
2 | distop 21177 indistop 21184 indistopon 21183 |
[Munkres] p. 77 | Example
3 | fctop 21186 fctop2 21187 |
[Munkres] p. 77 | Example
4 | cctop 21188 |
[Munkres] p.
78 | Definition of basis | df-bases 21128 isbasis3g 21131 |
[Munkres] p.
78 | Definition of a topology generated by a basis | df-topgen 16464 tgval2 21138 |
[Munkres] p.
79 | Remark | tgcl 21151 |
[Munkres] p. 80 | Lemma
2.1 | tgval3 21145 |
[Munkres] p. 80 | Lemma
2.2 | tgss2 21169 tgss3 21168 |
[Munkres] p. 81 | Lemma
2.3 | basgen 21170 basgen2 21171 |
[Munkres] p.
83 | Exercise 3 | topdifinf 33737 topdifinfeq 33738 topdifinffin 33736 topdifinfindis 33734 |
[Munkres] p.
89 | Definition of subspace topology | resttop 21342 |
[Munkres] p. 93 | Theorem
6.1(1) | 0cld 21220 topcld 21217 |
[Munkres] p. 93 | Theorem
6.1(2) | iincld 21221 |
[Munkres] p. 93 | Theorem
6.1(3) | uncld 21223 |
[Munkres] p.
94 | Definition of closure | clsval 21219 |
[Munkres] p.
94 | Definition of interior | ntrval 21218 |
[Munkres] p. 95 | Theorem
6.5(a) | clsndisj 21257 elcls 21255 |
[Munkres] p. 95 | Theorem
6.5(b) | elcls3 21265 |
[Munkres] p. 97 | Theorem
6.6 | clslp 21330 neindisj 21299 |
[Munkres] p.
97 | Corollary 6.7 | cldlp 21332 |
[Munkres] p.
97 | Definition of limit point | islp2 21327 lpval 21321 |
[Munkres] p.
98 | Definition of Hausdorff space | df-haus 21497 |
[Munkres] p.
102 | Definition of continuous function | df-cn 21409 iscn 21417 iscn2 21420 |
[Munkres] p.
107 | Theorem 7.2(g) | cncnp 21462 cncnp2 21463 cncnpi 21460 df-cnp 21410 iscnp 21419 iscnp2 21421 |
[Munkres] p.
127 | Theorem 10.1 | metcn 22725 |
[Munkres] p.
128 | Theorem 10.3 | metcn4 23486 |
[Nathanson]
p. 123 | Remark | reprgt 31244 reprinfz1 31245 reprlt 31242 |
[Nathanson]
p. 123 | Definition | df-repr 31232 |
[Nathanson]
p. 123 | Chapter 5.1 | circlemethnat 31264 |
[Nathanson]
p. 123 | Proposition | breprexp 31256 breprexpnat 31257 itgexpif 31229 |
[NielsenChuang] p. 195 | Equation
4.73 | unierri 29514 |
[OeSilva] p.
2042 | Section 2 | ax-bgbltosilva 42542 |
[Pfenning] p.
17 | Definition XM | natded 27814 |
[Pfenning] p.
17 | Definition NNC | natded 27814 notnotrd 131 |
[Pfenning] p.
17 | Definition ` `C | natded 27814 |
[Pfenning] p.
18 | Rule" | natded 27814 |
[Pfenning] p.
18 | Definition /\I | natded 27814 |
[Pfenning] p.
18 | Definition ` `E | natded 27814 natded 27814 natded 27814 natded 27814 natded 27814 |
[Pfenning] p.
18 | Definition ` `I | natded 27814 natded 27814 natded 27814 natded 27814 natded 27814 |
[Pfenning] p.
18 | Definition ` `EL | natded 27814 |
[Pfenning] p.
18 | Definition ` `ER | natded 27814 |
[Pfenning] p.
18 | Definition ` `Ea,u | natded 27814 |
[Pfenning] p.
18 | Definition ` `IR | natded 27814 |
[Pfenning] p.
18 | Definition ` `Ia | natded 27814 |
[Pfenning] p.
127 | Definition =E | natded 27814 |
[Pfenning] p.
127 | Definition =I | natded 27814 |
[Ponnusamy] p.
361 | Theorem 6.44 | cphip0l 23378 df-dip 28107 dip0l 28124 ip0l 20350 |
[Ponnusamy] p.
361 | Equation 6.45 | cphipval 23418 ipval 28109 |
[Ponnusamy] p.
362 | Equation I1 | dipcj 28120 ipcj 20348 |
[Ponnusamy] p.
362 | Equation I3 | cphdir 23381 dipdir 28248 ipdir 20353 ipdiri 28236 |
[Ponnusamy] p.
362 | Equation I4 | ipidsq 28116 nmsq 23370 |
[Ponnusamy] p.
362 | Equation 6.46 | ip0i 28231 |
[Ponnusamy] p.
362 | Equation 6.47 | ip1i 28233 |
[Ponnusamy] p.
362 | Equation 6.48 | ip2i 28234 |
[Ponnusamy] p.
363 | Equation I2 | cphass 23387 dipass 28251 ipass 20359 ipassi 28247 |
[Prugovecki] p. 186 | Definition of
bra | braval 29354 df-bra 29260 |
[Prugovecki] p. 376 | Equation
8.1 | df-kb 29261 kbval 29364 |
[PtakPulmannova] p. 66 | Proposition
3.2.17 | atomli 29792 |
[PtakPulmannova] p. 68 | Lemma
3.1.4 | df-pclN 35958 |
[PtakPulmannova] p. 68 | Lemma
3.2.20 | atcvat3i 29806 atcvat4i 29807 cvrat3 35512 cvrat4 35513 lsatcvat3 35122 |
[PtakPulmannova] p. 68 | Definition
3.2.18 | cvbr 29692 cvrval 35339 df-cv 29689 df-lcv 35089 lspsncv0 19513 |
[PtakPulmannova] p. 72 | Lemma
3.3.6 | pclfinN 35970 |
[PtakPulmannova] p. 74 | Lemma
3.3.10 | pclcmpatN 35971 |
[Quine] p. 16 | Definition
2.1 | df-clab 2812 rabid 3326 |
[Quine] p. 17 | Definition
2.1'' | dfsb7 2589 |
[Quine] p. 18 | Definition
2.7 | df-cleq 2818 |
[Quine] p. 19 | Definition
2.9 | conventions 27811 df-v 3416 |
[Quine] p. 34 | Theorem
5.1 | abeq2 2937 |
[Quine] p. 35 | Theorem
5.2 | abid1 2949 abid2f 2996 |
[Quine] p. 40 | Theorem
6.1 | sb5 2308 |
[Quine] p. 40 | Theorem
6.2 | sb56 2305 sb6 2307 |
[Quine] p. 41 | Theorem
6.3 | df-clel 2821 |
[Quine] p. 41 | Theorem
6.4 | eqid 2825 eqid1 27877 |
[Quine] p. 41 | Theorem
6.5 | eqcom 2832 |
[Quine] p. 42 | Theorem
6.6 | df-sbc 3663 |
[Quine] p. 42 | Theorem
6.7 | dfsbcq 3664 dfsbcq2 3665 |
[Quine] p. 43 | Theorem
6.8 | vex 3417 |
[Quine] p. 43 | Theorem
6.9 | isset 3424 |
[Quine] p. 44 | Theorem
7.3 | spcgf 3505 spcgv 3510 spcimgf 3503 |
[Quine] p. 44 | Theorem
6.11 | spsbc 3675 spsbcd 3676 |
[Quine] p. 44 | Theorem
6.12 | elex 3429 |
[Quine] p. 44 | Theorem
6.13 | elab 3571 elabg 3569 elabgf 3567 |
[Quine] p. 44 | Theorem
6.14 | noel 4150 |
[Quine] p. 48 | Theorem
7.2 | snprc 4473 |
[Quine] p. 48 | Definition
7.1 | df-pr 4402 df-sn 4400 |
[Quine] p. 49 | Theorem
7.4 | snss 4537 snssg 4536 |
[Quine] p. 49 | Theorem
7.5 | prss 4571 prssg 4570 |
[Quine] p. 49 | Theorem
7.6 | prid1 4517 prid1g 4515 prid2 4518 prid2g 4516 snid 4431
snidg 4429 |
[Quine] p. 51 | Theorem
7.12 | snex 5131 |
[Quine] p. 51 | Theorem
7.13 | prex 5132 |
[Quine] p. 53 | Theorem
8.2 | unisn 4676 unisnALT 39975 unisng 4675 |
[Quine] p. 53 | Theorem
8.3 | uniun 4681 |
[Quine] p. 54 | Theorem
8.6 | elssuni 4691 |
[Quine] p. 54 | Theorem
8.7 | uni0 4689 |
[Quine] p. 56 | Theorem
8.17 | uniabio 6100 |
[Quine] p.
56 | Definition 8.18 | dfaiota2 41977 dfiota2 6091 |
[Quine] p.
57 | Theorem 8.19 | aiotaval 41984 iotaval 6101 |
[Quine] p. 57 | Theorem
8.22 | iotanul 6105 |
[Quine] p. 58 | Theorem
8.23 | iotaex 6107 |
[Quine] p. 58 | Definition
9.1 | df-op 4406 |
[Quine] p. 61 | Theorem
9.5 | opabid 5210 opelopab 5225 opelopaba 5219 opelopabaf 5227 opelopabf 5228 opelopabg 5221 opelopabga 5216 opelopabgf 5223 oprabid 6941 |
[Quine] p. 64 | Definition
9.11 | df-xp 5352 |
[Quine] p. 64 | Definition
9.12 | df-cnv 5354 |
[Quine] p. 64 | Definition
9.15 | df-id 5252 |
[Quine] p. 65 | Theorem
10.3 | fun0 6191 |
[Quine] p. 65 | Theorem
10.4 | funi 6159 |
[Quine] p. 65 | Theorem
10.5 | funsn 6179 funsng 6177 |
[Quine] p. 65 | Definition
10.1 | df-fun 6129 |
[Quine] p. 65 | Definition
10.2 | args 5738 dffv4 6434 |
[Quine] p. 68 | Definition
10.11 | conventions 27811 df-fv 6135 fv2 6432 |
[Quine] p. 124 | Theorem
17.3 | nn0opth2 13359 nn0opth2i 13358 nn0opthi 13357 omopthi 8009 |
[Quine] p. 177 | Definition
25.2 | df-rdg 7777 |
[Quine] p. 232 | Equation
i | carddom 9698 |
[Quine] p. 284 | Axiom
39(vi) | funimaex 6213 funimaexg 6212 |
[Quine] p. 331 | Axiom
system NF | ru 3661 |
[ReedSimon]
p. 36 | Definition (iii) | ax-his3 28492 |
[ReedSimon] p.
63 | Exercise 4(a) | df-dip 28107 polid 28567 polid2i 28565 polidi 28566 |
[ReedSimon] p.
63 | Exercise 4(b) | df-ph 28219 |
[ReedSimon]
p. 195 | Remark | lnophm 29429 lnophmi 29428 |
[Retherford] p. 49 | Exercise
1(i) | leopadd 29542 |
[Retherford] p. 49 | Exercise
1(ii) | leopmul 29544 leopmuli 29543 |
[Retherford] p. 49 | Exercise
1(iv) | leoptr 29547 |
[Retherford] p. 49 | Definition
VI.1 | df-leop 29262 leoppos 29536 |
[Retherford] p. 49 | Exercise
1(iii) | leoptri 29546 |
[Retherford] p. 49 | Definition of
operator ordering | leop3 29535 |
[Roman] p.
4 | Definition | df-dmat 20671 df-dmatalt 43048 |
[Roman] p.
18 | Part Preliminaries | df-rng0 42736 |
[Roman] p. 19 | Part
Preliminaries | df-ring 18910 |
[Roman] p.
46 | Theorem 1.6 | isldepslvec2 43135 |
[Roman] p.
112 | Note | isldepslvec2 43135 ldepsnlinc 43158 zlmodzxznm 43147 |
[Roman] p.
112 | Example | zlmodzxzequa 43146 zlmodzxzequap 43149 zlmodzxzldep 43154 |
[Roman] p. 170 | Theorem
7.8 | cayleyhamilton 21072 |
[Rosenlicht] p. 80 | Theorem | heicant 33983 |
[Rosser] p.
281 | Definition | df-op 4406 |
[RosserSchoenfeld] p. 71 | Theorem
12. | ax-ros335 31268 |
[RosserSchoenfeld] p. 71 | Theorem
13. | ax-ros336 31269 |
[Rotman] p.
28 | Remark | pgrpgt2nabl 43008 pmtr3ncom 18252 |
[Rotman] p. 31 | Theorem
3.4 | symggen2 18248 |
[Rotman] p. 42 | Theorem
3.15 | cayley 18191 cayleyth 18192 |
[Rudin] p. 164 | Equation
27 | efcan 15205 |
[Rudin] p. 164 | Equation
30 | efzval 15211 |
[Rudin] p. 167 | Equation
48 | absefi 15305 |
[Sanford] p.
39 | Remark | ax-mp 5 mto 189 |
[Sanford] p. 39 | Rule
3 | mtpxor 1870 |
[Sanford] p. 39 | Rule
4 | mptxor 1868 |
[Sanford] p. 40 | Rule
1 | mptnan 1867 |
[Schechter] p.
51 | Definition of antisymmetry | intasym 5757 |
[Schechter] p.
51 | Definition of irreflexivity | intirr 5760 |
[Schechter] p.
51 | Definition of symmetry | cnvsym 5756 |
[Schechter] p.
51 | Definition of transitivity | cotr 5753 |
[Schechter] p.
78 | Definition of Moore collection of sets | df-mre 16606 |
[Schechter] p.
79 | Definition of Moore closure | df-mrc 16607 |
[Schechter] p.
82 | Section 4.5 | df-mrc 16607 |
[Schechter] p.
84 | Definition (A) of an algebraic closure system | df-acs 16609 |
[Schechter] p.
139 | Definition AC3 | dfac9 9280 |
[Schechter]
p. 141 | Definition (MC) | dfac11 38470 |
[Schechter] p.
149 | Axiom DC1 | ax-dc 9590 axdc3 9598 |
[Schechter] p.
187 | Definition of ring with unit | isring 18912 isrngo 34233 |
[Schechter]
p. 276 | Remark 11.6.e | span0 28952 |
[Schechter]
p. 276 | Definition of span | df-span 28719 spanval 28743 |
[Schechter] p.
428 | Definition 15.35 | bastop1 21175 |
[Schwabhauser] p.
10 | Axiom A1 | axcgrrflx 26220 axtgcgrrflx 25781 |
[Schwabhauser] p.
10 | Axiom A2 | axcgrtr 26221 |
[Schwabhauser] p.
10 | Axiom A3 | axcgrid 26222 axtgcgrid 25782 |
[Schwabhauser] p.
10 | Axioms A1 to A3 | df-trkgc 25767 |
[Schwabhauser] p.
11 | Axiom A4 | axsegcon 26233 axtgsegcon 25783 df-trkgcb 25769 |
[Schwabhauser] p.
11 | Axiom A5 | ax5seg 26244 axtg5seg 25784 df-trkgcb 25769 |
[Schwabhauser] p.
11 | Axiom A6 | axbtwnid 26245 axtgbtwnid 25785 df-trkgb 25768 |
[Schwabhauser] p.
12 | Axiom A7 | axpasch 26247 axtgpasch 25786 df-trkgb 25768 |
[Schwabhauser] p.
12 | Axiom A8 | axlowdim2 26266 df-trkg2d 31288 |
[Schwabhauser] p.
13 | Axiom A8 | axtglowdim2 25789 |
[Schwabhauser] p.
13 | Axiom A9 | axtgupdim2 25790 df-trkg2d 31288 |
[Schwabhauser] p.
13 | Axiom A10 | axeuclid 26269 axtgeucl 25791 df-trkge 25770 |
[Schwabhauser] p.
13 | Axiom A11 | axcont 26282 axtgcont 25788 axtgcont1 25787 df-trkgb 25768 |
[Schwabhauser] p. 27 | Theorem
2.1 | cgrrflx 32628 |
[Schwabhauser] p. 27 | Theorem
2.2 | cgrcomim 32630 |
[Schwabhauser] p. 27 | Theorem
2.3 | cgrtr 32633 |
[Schwabhauser] p. 27 | Theorem
2.4 | cgrcoml 32637 |
[Schwabhauser] p. 27 | Theorem
2.5 | cgrcomr 32638 tgcgrcomimp 25796 tgcgrcoml 25798 tgcgrcomr 25797 |
[Schwabhauser] p. 28 | Theorem
2.8 | cgrtriv 32643 tgcgrtriv 25803 |
[Schwabhauser] p. 28 | Theorem
2.10 | 5segofs 32647 tg5segofs 31296 |
[Schwabhauser] p. 28 | Definition
2.10 | df-afs 31293 df-ofs 32624 |
[Schwabhauser] p. 29 | Theorem
2.11 | cgrextend 32649 tgcgrextend 25804 |
[Schwabhauser] p. 29 | Theorem
2.12 | segconeq 32651 tgsegconeq 25805 |
[Schwabhauser] p. 30 | Theorem
3.1 | btwnouttr2 32663 btwntriv2 32653 tgbtwntriv2 25806 |
[Schwabhauser] p. 30 | Theorem
3.2 | btwncomim 32654 tgbtwncom 25807 |
[Schwabhauser] p. 30 | Theorem
3.3 | btwntriv1 32657 tgbtwntriv1 25810 |
[Schwabhauser] p. 30 | Theorem
3.4 | btwnswapid 32658 tgbtwnswapid 25811 |
[Schwabhauser] p. 30 | Theorem
3.5 | btwnexch2 32664 btwnintr 32660 tgbtwnexch2 25815 tgbtwnintr 25812 |
[Schwabhauser] p. 30 | Theorem
3.6 | btwnexch 32666 btwnexch3 32661 tgbtwnexch 25817 tgbtwnexch3 25813 |
[Schwabhauser] p. 30 | Theorem
3.7 | btwnouttr 32665 tgbtwnouttr 25816 tgbtwnouttr2 25814 |
[Schwabhauser] p.
32 | Theorem 3.13 | axlowdim1 26265 |
[Schwabhauser] p. 32 | Theorem
3.14 | btwndiff 32668 tgbtwndiff 25825 |
[Schwabhauser] p.
33 | Theorem 3.17 | tgtrisegint 25818 trisegint 32669 |
[Schwabhauser] p. 34 | Theorem
4.2 | ifscgr 32685 tgifscgr 25827 |
[Schwabhauser] p.
34 | Theorem 4.11 | colcom 25877 colrot1 25878 colrot2 25879 lncom 25941 lnrot1 25942 lnrot2 25943 |
[Schwabhauser] p. 34 | Definition
4.1 | df-ifs 32681 |
[Schwabhauser] p. 35 | Theorem
4.3 | cgrsub 32686 tgcgrsub 25828 |
[Schwabhauser] p. 35 | Theorem
4.5 | cgrxfr 32696 tgcgrxfr 25837 |
[Schwabhauser] p.
35 | Statement 4.4 | ercgrg 25836 |
[Schwabhauser] p. 35 | Definition
4.4 | df-cgr3 32682 df-cgrg 25830 |
[Schwabhauser] p.
35 | Definition instead (given | df-cgrg 25830 |
[Schwabhauser] p. 36 | Theorem
4.6 | btwnxfr 32697 tgbtwnxfr 25849 |
[Schwabhauser] p. 36 | Theorem
4.11 | colinearperm1 32703 colinearperm2 32705 colinearperm3 32704 colinearperm4 32706 colinearperm5 32707 |
[Schwabhauser] p.
36 | Definition 4.8 | df-ismt 25852 |
[Schwabhauser] p. 36 | Definition
4.10 | df-colinear 32680 tgellng 25872 tglng 25865 |
[Schwabhauser] p. 37 | Theorem
4.12 | colineartriv1 32708 |
[Schwabhauser] p. 37 | Theorem
4.13 | colinearxfr 32716 lnxfr 25885 |
[Schwabhauser] p. 37 | Theorem
4.14 | lineext 32717 lnext 25886 |
[Schwabhauser] p. 37 | Theorem
4.16 | fscgr 32721 tgfscgr 25887 |
[Schwabhauser] p. 37 | Theorem
4.17 | linecgr 32722 lncgr 25888 |
[Schwabhauser] p. 37 | Definition
4.15 | df-fs 32683 |
[Schwabhauser] p. 38 | Theorem
4.18 | lineid 32724 lnid 25889 |
[Schwabhauser] p. 38 | Theorem
4.19 | idinside 32725 tgidinside 25890 |
[Schwabhauser] p. 39 | Theorem
5.1 | btwnconn1 32742 tgbtwnconn1 25894 |
[Schwabhauser] p. 41 | Theorem
5.2 | btwnconn2 32743 tgbtwnconn2 25895 |
[Schwabhauser] p. 41 | Theorem
5.3 | btwnconn3 32744 tgbtwnconn3 25896 |
[Schwabhauser] p. 41 | Theorem
5.5 | brsegle2 32750 |
[Schwabhauser] p. 41 | Definition
5.4 | df-segle 32748 legov 25904 |
[Schwabhauser] p.
41 | Definition 5.5 | legov2 25905 |
[Schwabhauser] p.
42 | Remark 5.13 | legso 25918 |
[Schwabhauser] p. 42 | Theorem
5.6 | seglecgr12im 32751 |
[Schwabhauser] p. 42 | Theorem
5.7 | seglerflx 32753 |
[Schwabhauser] p. 42 | Theorem
5.8 | segletr 32755 |
[Schwabhauser] p. 42 | Theorem
5.9 | segleantisym 32756 |
[Schwabhauser] p. 42 | Theorem
5.10 | seglelin 32757 |
[Schwabhauser] p. 42 | Theorem
5.11 | seglemin 32754 |
[Schwabhauser] p. 42 | Theorem
5.12 | colinbtwnle 32759 |
[Schwabhauser] p.
42 | Proposition 5.7 | legid 25906 |
[Schwabhauser] p.
42 | Proposition 5.8 | legtrd 25908 |
[Schwabhauser] p.
42 | Proposition 5.9 | legtri3 25909 |
[Schwabhauser] p.
42 | Proposition 5.10 | legtrid 25910 |
[Schwabhauser] p.
42 | Proposition 5.11 | leg0 25911 |
[Schwabhauser] p. 43 | Theorem
6.2 | btwnoutside 32766 |
[Schwabhauser] p. 43 | Theorem
6.3 | broutsideof3 32767 |
[Schwabhauser] p. 43 | Theorem
6.4 | broutsideof 32762 df-outsideof 32761 |
[Schwabhauser] p. 43 | Definition
6.1 | broutsideof2 32763 ishlg 25921 |
[Schwabhauser] p.
44 | Theorem 6.4 | hlln 25926 |
[Schwabhauser] p.
44 | Theorem 6.5 | hlid 25928 outsideofrflx 32768 |
[Schwabhauser] p.
44 | Theorem 6.6 | hlcomb 25922 hlcomd 25923 outsideofcom 32769 |
[Schwabhauser] p.
44 | Theorem 6.7 | hltr 25929 outsideoftr 32770 |
[Schwabhauser] p.
44 | Theorem 6.11 | hlcgreu 25937 outsideofeu 32772 |
[Schwabhauser] p. 44 | Definition
6.8 | df-ray 32779 |
[Schwabhauser] p. 45 | Part
2 | df-lines2 32780 |
[Schwabhauser] p. 45 | Theorem
6.13 | outsidele 32773 |
[Schwabhauser] p. 45 | Theorem
6.15 | lineunray 32788 |
[Schwabhauser] p. 45 | Theorem
6.16 | lineelsb2 32789 tglineelsb2 25951 |
[Schwabhauser] p. 45 | Theorem
6.17 | linecom 32791 linerflx1 32790 linerflx2 32792 tglinecom 25954 tglinerflx1 25952 tglinerflx2 25953 |
[Schwabhauser] p. 45 | Theorem
6.18 | linethru 32794 tglinethru 25955 |
[Schwabhauser] p. 45 | Definition
6.14 | df-line2 32778 tglng 25865 |
[Schwabhauser] p.
45 | Proposition 6.13 | legbtwn 25913 |
[Schwabhauser] p. 46 | Theorem
6.19 | linethrueu 32797 tglinethrueu 25958 |
[Schwabhauser] p. 46 | Theorem
6.21 | lineintmo 32798 tglineineq 25962 tglineinteq 25964 tglineintmo 25961 |
[Schwabhauser] p.
46 | Theorem 6.23 | colline 25968 |
[Schwabhauser] p.
46 | Theorem 6.24 | tglowdim2l 25969 |
[Schwabhauser] p.
46 | Theorem 6.25 | tglowdim2ln 25970 |
[Schwabhauser] p.
49 | Theorem 7.3 | mirinv 25985 |
[Schwabhauser] p.
49 | Theorem 7.7 | mirmir 25981 |
[Schwabhauser] p.
49 | Theorem 7.8 | mirreu3 25973 |
[Schwabhauser] p.
49 | Definition 7.5 | df-mir 25972 ismir 25978 mirbtwn 25977 mircgr 25976 mirfv 25975 mirval 25974 |
[Schwabhauser] p.
50 | Theorem 7.8 | mirreu 25983 |
[Schwabhauser] p.
50 | Theorem 7.9 | mireq 25984 |
[Schwabhauser] p.
50 | Theorem 7.10 | mirinv 25985 |
[Schwabhauser] p.
50 | Theorem 7.11 | mirf1o 25988 |
[Schwabhauser] p.
50 | Theorem 7.13 | miriso 25989 |
[Schwabhauser] p.
51 | Theorem 7.14 | mirmot 25994 |
[Schwabhauser] p.
51 | Theorem 7.15 | mirbtwnb 25991 mirbtwni 25990 |
[Schwabhauser] p.
51 | Theorem 7.16 | mircgrs 25992 |
[Schwabhauser] p.
51 | Theorem 7.17 | miduniq 26004 |
[Schwabhauser] p.
52 | Lemma 7.21 | symquadlem 26008 |
[Schwabhauser] p.
52 | Theorem 7.18 | miduniq1 26005 |
[Schwabhauser] p.
52 | Theorem 7.19 | miduniq2 26006 |
[Schwabhauser] p.
52 | Theorem 7.20 | colmid 26007 |
[Schwabhauser] p.
53 | Lemma 7.22 | krippen 26010 |
[Schwabhauser] p.
55 | Lemma 7.25 | midexlem 26011 |
[Schwabhauser] p.
57 | Theorem 8.2 | ragcom 26017 |
[Schwabhauser] p.
57 | Definition 8.1 | df-rag 26013 israg 26016 |
[Schwabhauser] p.
58 | Theorem 8.3 | ragcol 26018 |
[Schwabhauser] p.
58 | Theorem 8.4 | ragmir 26019 |
[Schwabhauser] p.
58 | Theorem 8.5 | ragtrivb 26021 |
[Schwabhauser] p.
58 | Theorem 8.6 | ragflat2 26022 |
[Schwabhauser] p.
58 | Theorem 8.7 | ragflat 26023 |
[Schwabhauser] p.
58 | Theorem 8.8 | ragtriva 26024 |
[Schwabhauser] p.
58 | Theorem 8.9 | ragflat3 26025 ragncol 26028 |
[Schwabhauser] p.
58 | Theorem 8.10 | ragcgr 26026 |
[Schwabhauser] p.
59 | Theorem 8.12 | perpcom 26032 |
[Schwabhauser] p.
59 | Theorem 8.13 | ragperp 26036 |
[Schwabhauser] p.
59 | Theorem 8.14 | perpneq 26033 |
[Schwabhauser] p.
59 | Definition 8.11 | df-perpg 26015 isperp 26031 |
[Schwabhauser] p.
59 | Definition 8.13 | isperp2 26034 |
[Schwabhauser] p.
60 | Theorem 8.18 | foot 26038 |
[Schwabhauser] p.
62 | Lemma 8.20 | colperpexlem1 26046 colperpexlem2 26047 |
[Schwabhauser] p.
63 | Theorem 8.21 | colperpex 26049 colperpexlem3 26048 |
[Schwabhauser] p.
64 | Theorem 8.22 | mideu 26054 midex 26053 |
[Schwabhauser] p.
66 | Lemma 8.24 | opphllem 26051 |
[Schwabhauser] p.
67 | Theorem 9.2 | oppcom 26060 |
[Schwabhauser] p.
67 | Definition 9.1 | islnopp 26055 |
[Schwabhauser] p.
68 | Lemma 9.3 | opphllem2 26064 |
[Schwabhauser] p.
68 | Lemma 9.4 | opphllem5 26067 opphllem6 26068 |
[Schwabhauser] p.
69 | Theorem 9.5 | opphl 26070 |
[Schwabhauser] p.
69 | Theorem 9.6 | axtgpasch 25786 |
[Schwabhauser] p.
70 | Theorem 9.6 | outpasch 26071 |
[Schwabhauser] p.
71 | Theorem 9.8 | lnopp2hpgb 26079 |
[Schwabhauser] p.
71 | Definition 9.7 | df-hpg 26074 hpgbr 26076 |
[Schwabhauser] p.
72 | Lemma 9.10 | hpgerlem 26081 |
[Schwabhauser] p.
72 | Theorem 9.9 | lnoppnhpg 26080 |
[Schwabhauser] p.
72 | Theorem 9.11 | hpgid 26082 |
[Schwabhauser] p.
72 | Theorem 9.12 | hpgcom 26083 |
[Schwabhauser] p.
72 | Theorem 9.13 | hpgtr 26084 |
[Schwabhauser] p.
73 | Theorem 9.18 | colopp 26085 |
[Schwabhauser] p.
73 | Theorem 9.19 | colhp 26086 |
[Schwabhauser] p.
88 | Theorem 10.2 | lmieu 26100 |
[Schwabhauser] p.
88 | Definition 10.1 | df-mid 26090 |
[Schwabhauser] p.
89 | Theorem 10.4 | lmicom 26104 |
[Schwabhauser] p.
89 | Theorem 10.5 | lmilmi 26105 |
[Schwabhauser] p.
89 | Theorem 10.6 | lmireu 26106 |
[Schwabhauser] p.
89 | Theorem 10.7 | lmieq 26107 |
[Schwabhauser] p.
89 | Theorem 10.8 | lmiinv 26108 |
[Schwabhauser] p.
89 | Theorem 10.9 | lmif1o 26111 |
[Schwabhauser] p.
89 | Theorem 10.10 | lmiiso 26113 |
[Schwabhauser] p.
89 | Definition 10.3 | df-lmi 26091 |
[Schwabhauser] p.
90 | Theorem 10.11 | lmimot 26114 |
[Schwabhauser] p.
91 | Theorem 10.12 | hypcgr 26117 |
[Schwabhauser] p.
92 | Theorem 10.14 | lmiopp 26118 |
[Schwabhauser] p.
92 | Theorem 10.15 | lnperpex 26119 |
[Schwabhauser] p.
92 | Theorem 10.16 | trgcopy 26120 trgcopyeu 26122 |
[Schwabhauser] p.
95 | Definition 11.2 | dfcgra2 26145 |
[Schwabhauser] p.
95 | Definition 11.3 | iscgra 26125 |
[Schwabhauser] p.
95 | Proposition 11.4 | cgracgr 26134 |
[Schwabhauser] p.
95 | Proposition 11.10 | cgrahl1 26132 cgrahl2 26133 |
[Schwabhauser] p.
96 | Theorem 11.6 | cgraid 26135 |
[Schwabhauser] p.
96 | Theorem 11.9 | cgraswap 26136 |
[Schwabhauser] p.
97 | Theorem 11.7 | cgracom 26138 |
[Schwabhauser] p.
97 | Theorem 11.8 | cgratr 26139 |
[Schwabhauser] p.
97 | Theorem 11.21 | cgrabtwn 26141 cgrahl 26142 |
[Schwabhauser] p.
98 | Theorem 11.13 | sacgr 26146 |
[Schwabhauser] p.
98 | Theorem 11.14 | oacgr 26148 |
[Schwabhauser] p.
98 | Theorem 11.15 | acopy 26149 acopyeu 26150 |
[Schwabhauser] p.
101 | Theorem 11.24 | inagswap 26155 |
[Schwabhauser] p.
101 | Theorem 11.25 | inaghl 26156 |
[Schwabhauser] p.
101 | Property for point ` ` to lie in the angle ` ` Defnition
11.23 | isinag 26154 |
[Schwabhauser] p.
102 | Lemma 11.28 | cgrg3col4 26159 |
[Schwabhauser] p.
102 | Definition 11.27 | df-leag 26157 isleag 26158 |
[Schwabhauser] p.
107 | Theorem 11.49 | tgsas 26161 tgsas1 26160 tgsas2 26162 tgsas3 26163 |
[Schwabhauser] p.
108 | Theorem 11.50 | tgasa 26165 tgasa1 26164 |
[Schwabhauser] p.
109 | Theorem 11.51 | tgsss1 26166 tgsss2 26167 tgsss3 26168 |
[Shapiro] p.
230 | Theorem 6.5.1 | dchrhash 25416 dchrsum 25414 dchrsum2 25413 sumdchr 25417 |
[Shapiro] p.
232 | Theorem 6.5.2 | dchr2sum 25418 sum2dchr 25419 |
[Shapiro], p. 199 | Lemma
6.1C.2 | ablfacrp 18826 ablfacrp2 18827 |
[Shapiro], p.
328 | Equation 9.2.4 | vmasum 25361 |
[Shapiro], p.
329 | Equation 9.2.7 | logfac2 25362 |
[Shapiro], p.
329 | Equation 9.2.9 | logfacrlim 25369 |
[Shapiro], p.
331 | Equation 9.2.13 | vmadivsum 25591 |
[Shapiro], p.
331 | Equation 9.2.14 | rplogsumlem2 25594 |
[Shapiro], p.
336 | Exercise 9.1.7 | vmalogdivsum 25648 vmalogdivsum2 25647 |
[Shapiro], p.
375 | Theorem 9.4.1 | dirith 25638 dirith2 25637 |
[Shapiro], p.
375 | Equation 9.4.3 | rplogsum 25636 rpvmasum 25635 rpvmasum2 25621 |
[Shapiro], p.
376 | Equation 9.4.7 | rpvmasumlem 25596 |
[Shapiro], p.
376 | Equation 9.4.8 | dchrvmasum 25634 |
[Shapiro], p. 377 | Lemma
9.4.1 | dchrisum 25601 dchrisumlem1 25598 dchrisumlem2 25599 dchrisumlem3 25600 dchrisumlema 25597 |
[Shapiro], p.
377 | Equation 9.4.11 | dchrvmasumlem1 25604 |
[Shapiro], p.
379 | Equation 9.4.16 | dchrmusum 25633 dchrmusumlem 25631 dchrvmasumlem 25632 |
[Shapiro], p. 380 | Lemma
9.4.2 | dchrmusum2 25603 |
[Shapiro], p. 380 | Lemma
9.4.3 | dchrvmasum2lem 25605 |
[Shapiro], p. 382 | Lemma
9.4.4 | dchrisum0 25629 dchrisum0re 25622 dchrisumn0 25630 |
[Shapiro], p.
382 | Equation 9.4.27 | dchrisum0fmul 25615 |
[Shapiro], p.
382 | Equation 9.4.29 | dchrisum0flb 25619 |
[Shapiro], p.
383 | Equation 9.4.30 | dchrisum0fno1 25620 |
[Shapiro], p.
403 | Equation 10.1.16 | pntrsumbnd 25675 pntrsumbnd2 25676 pntrsumo1 25674 |
[Shapiro], p.
405 | Equation 10.2.1 | mudivsum 25639 |
[Shapiro], p.
406 | Equation 10.2.6 | mulogsum 25641 |
[Shapiro], p.
407 | Equation 10.2.7 | mulog2sumlem1 25643 |
[Shapiro], p.
407 | Equation 10.2.8 | mulog2sum 25646 |
[Shapiro], p.
418 | Equation 10.4.6 | logsqvma 25651 |
[Shapiro], p.
418 | Equation 10.4.8 | logsqvma2 25652 |
[Shapiro], p.
419 | Equation 10.4.10 | selberg 25657 |
[Shapiro], p.
420 | Equation 10.4.12 | selberg2lem 25659 |
[Shapiro], p.
420 | Equation 10.4.14 | selberg2 25660 |
[Shapiro], p.
422 | Equation 10.6.7 | selberg3 25668 |
[Shapiro], p.
422 | Equation 10.4.20 | selberg4lem1 25669 |
[Shapiro], p.
422 | Equation 10.4.21 | selberg3lem1 25666 selberg3lem2 25667 |
[Shapiro], p.
422 | Equation 10.4.23 | selberg4 25670 |
[Shapiro], p.
427 | Theorem 10.5.2 | chpdifbnd 25664 |
[Shapiro], p.
428 | Equation 10.6.2 | selbergr 25677 |
[Shapiro], p.
429 | Equation 10.6.8 | selberg3r 25678 |
[Shapiro], p.
430 | Equation 10.6.11 | selberg4r 25679 |
[Shapiro], p.
431 | Equation 10.6.15 | pntrlog2bnd 25693 |
[Shapiro], p.
434 | Equation 10.6.27 | pntlema 25705 pntlemb 25706 pntlemc 25704 pntlemd 25703 pntlemg 25707 |
[Shapiro], p.
435 | Equation 10.6.29 | pntlema 25705 |
[Shapiro], p. 436 | Lemma
10.6.1 | pntpbnd 25697 |
[Shapiro], p. 436 | Lemma
10.6.2 | pntibnd 25702 |
[Shapiro], p.
436 | Equation 10.6.34 | pntlema 25705 |
[Shapiro], p.
436 | Equation 10.6.35 | pntlem3 25718 pntleml 25720 |
[Stoll] p. 13 | Definition
corresponds to | dfsymdif3 4124 |
[Stoll] p. 16 | Exercise
4.4 | 0dif 4204 dif0 4182 |
[Stoll] p. 16 | Exercise
4.8 | difdifdir 4281 |
[Stoll] p. 17 | Theorem
5.1(5) | unvdif 4267 |
[Stoll] p. 19 | Theorem
5.2(13) | undm 4117 |
[Stoll] p. 19 | Theorem
5.2(13') | indm 4118 |
[Stoll] p.
20 | Remark | invdif 4100 |
[Stoll] p. 25 | Definition
of ordered triple | df-ot 4408 |
[Stoll] p.
43 | Definition | uniiun 4795 |
[Stoll] p.
44 | Definition | intiin 4796 |
[Stoll] p.
45 | Definition | df-iin 4745 |
[Stoll] p. 45 | Definition
indexed union | df-iun 4744 |
[Stoll] p. 176 | Theorem
3.4(27) | iman 392 |
[Stoll] p. 262 | Example
4.1 | dfsymdif3 4124 |
[Strang] p.
242 | Section 6.3 | expgrowth 39369 |
[Suppes] p. 22 | Theorem
2 | eq0 4160 eq0f 4157 |
[Suppes] p. 22 | Theorem
4 | eqss 3842 eqssd 3844 eqssi 3843 |
[Suppes] p. 23 | Theorem
5 | ss0 4201 ss0b 4200 |
[Suppes] p. 23 | Theorem
6 | sstr 3835 sstrALT2 39884 |
[Suppes] p. 23 | Theorem
7 | pssirr 3935 |
[Suppes] p. 23 | Theorem
8 | pssn2lp 3936 |
[Suppes] p. 23 | Theorem
9 | psstr 3939 |
[Suppes] p. 23 | Theorem
10 | pssss 3930 |
[Suppes] p. 25 | Theorem
12 | elin 4025 elun 3982 |
[Suppes] p. 26 | Theorem
15 | inidm 4049 |
[Suppes] p. 26 | Theorem
16 | in0 4195 |
[Suppes] p. 27 | Theorem
23 | unidm 3985 |
[Suppes] p. 27 | Theorem
24 | un0 4194 |
[Suppes] p. 27 | Theorem
25 | ssun1 4005 |
[Suppes] p. 27 | Theorem
26 | ssequn1 4012 |
[Suppes] p. 27 | Theorem
27 | unss 4016 |
[Suppes] p. 27 | Theorem
28 | indir 4107 |
[Suppes] p. 27 | Theorem
29 | undir 4108 |
[Suppes] p. 28 | Theorem
32 | difid 4180 |
[Suppes] p. 29 | Theorem
33 | difin 4093 |
[Suppes] p. 29 | Theorem
34 | indif 4101 |
[Suppes] p. 29 | Theorem
35 | undif1 4268 |
[Suppes] p. 29 | Theorem
36 | difun2 4273 |
[Suppes] p. 29 | Theorem
37 | difin0 4266 |
[Suppes] p. 29 | Theorem
38 | disjdif 4265 |
[Suppes] p. 29 | Theorem
39 | difundi 4111 |
[Suppes] p. 29 | Theorem
40 | difindi 4113 |
[Suppes] p. 30 | Theorem
41 | nalset 5022 |
[Suppes] p. 39 | Theorem
61 | uniss 4683 |
[Suppes] p. 39 | Theorem
65 | uniop 5203 |
[Suppes] p. 41 | Theorem
70 | intsn 4735 |
[Suppes] p. 42 | Theorem
71 | intpr 4732 intprg 4733 |
[Suppes] p. 42 | Theorem
73 | op1stb 5162 |
[Suppes] p. 42 | Theorem
78 | intun 4731 |
[Suppes] p.
44 | Definition 15(a) | dfiun2 4776 dfiun2g 4774 |
[Suppes] p.
44 | Definition 15(b) | dfiin2 4777 |
[Suppes] p. 47 | Theorem
86 | elpw 4386 elpw2 5052 elpw2g 5051 elpwg 4388 elpwgdedVD 39966 |
[Suppes] p. 47 | Theorem
87 | pwid 4396 |
[Suppes] p. 47 | Theorem
89 | pw0 4563 |
[Suppes] p. 48 | Theorem
90 | pwpw0 4564 |
[Suppes] p. 52 | Theorem
101 | xpss12 5361 |
[Suppes] p. 52 | Theorem
102 | xpindi 5492 xpindir 5493 |
[Suppes] p. 52 | Theorem
103 | xpundi 5408 xpundir 5409 |
[Suppes] p. 54 | Theorem
105 | elirrv 8777 |
[Suppes] p. 58 | Theorem
2 | relss 5445 |
[Suppes] p. 59 | Theorem
4 | eldm 5557 eldm2 5558 eldm2g 5556 eldmg 5555 |
[Suppes] p.
59 | Definition 3 | df-dm 5356 |
[Suppes] p. 60 | Theorem
6 | dmin 5568 |
[Suppes] p. 60 | Theorem
8 | rnun 5786 |
[Suppes] p. 60 | Theorem
9 | rnin 5787 |
[Suppes] p.
60 | Definition 4 | dfrn2 5547 |
[Suppes] p. 61 | Theorem
11 | brcnv 5541 brcnvg 5538 |
[Suppes] p. 62 | Equation
5 | elcnv 5535 elcnv2 5536 |
[Suppes] p. 62 | Theorem
12 | relcnv 5748 |
[Suppes] p. 62 | Theorem
15 | cnvin 5785 |
[Suppes] p. 62 | Theorem
16 | cnvun 5783 |
[Suppes] p.
63 | Definition | dftrrels2 34864 |
[Suppes] p. 63 | Theorem
20 | co02 5894 |
[Suppes] p. 63 | Theorem
21 | dmcoss 5622 |
[Suppes] p.
63 | Definition 7 | df-co 5355 |
[Suppes] p. 64 | Theorem
26 | cnvco 5544 |
[Suppes] p. 64 | Theorem
27 | coass 5899 |
[Suppes] p. 65 | Theorem
31 | resundi 5651 |
[Suppes] p. 65 | Theorem
34 | elima 5716 elima2 5717 elima3 5718 elimag 5715 |
[Suppes] p. 65 | Theorem
35 | imaundi 5790 |
[Suppes] p. 66 | Theorem
40 | dminss 5792 |
[Suppes] p. 66 | Theorem
41 | imainss 5793 |
[Suppes] p. 67 | Exercise
11 | cnvxp 5796 |
[Suppes] p.
81 | Definition 34 | dfec2 8017 |
[Suppes] p. 82 | Theorem
72 | elec 8056 elecALTV 34579 elecg 8055 |
[Suppes] p.
82 | Theorem 73 | eqvrelth 34896 erth 8061
erth2 8062 |
[Suppes] p.
83 | Theorem 74 | eqvreldisj 34899 erdisj 8064 |
[Suppes] p. 89 | Theorem
96 | map0b 8168 |
[Suppes] p. 89 | Theorem
97 | map0 8171 map0g 8169 |
[Suppes] p. 89 | Theorem
98 | mapsn 8172 mapsnd 8170 |
[Suppes] p. 89 | Theorem
99 | mapss 8173 |
[Suppes] p.
91 | Definition 12(ii) | alephsuc 9211 |
[Suppes] p.
91 | Definition 12(iii) | alephlim 9210 |
[Suppes] p. 92 | Theorem
1 | enref 8261 enrefg 8260 |
[Suppes] p. 92 | Theorem
2 | ensym 8277 ensymb 8276 ensymi 8278 |
[Suppes] p. 92 | Theorem
3 | entr 8280 |
[Suppes] p. 92 | Theorem
4 | unen 8315 |
[Suppes] p. 94 | Theorem
15 | endom 8255 |
[Suppes] p. 94 | Theorem
16 | ssdomg 8274 |
[Suppes] p. 94 | Theorem
17 | domtr 8281 |
[Suppes] p. 95 | Theorem
18 | sbth 8355 |
[Suppes] p. 97 | Theorem
23 | canth2 8388 canth2g 8389 |
[Suppes] p.
97 | Definition 3 | brsdom2 8359 df-sdom 8231 dfsdom2 8358 |
[Suppes] p. 97 | Theorem
21(i) | sdomirr 8372 |
[Suppes] p. 97 | Theorem
22(i) | domnsym 8361 |
[Suppes] p. 97 | Theorem
21(ii) | sdomnsym 8360 |
[Suppes] p. 97 | Theorem
22(ii) | domsdomtr 8370 |
[Suppes] p. 97 | Theorem
22(iv) | brdom2 8258 |
[Suppes] p. 97 | Theorem
21(iii) | sdomtr 8373 |
[Suppes] p. 97 | Theorem
22(iii) | sdomdomtr 8368 |
[Suppes] p. 98 | Exercise
4 | fundmen 8302 fundmeng 8303 |
[Suppes] p. 98 | Exercise
6 | xpdom3 8333 |
[Suppes] p. 98 | Exercise
11 | sdomentr 8369 |
[Suppes] p. 104 | Theorem
37 | fofi 8527 |
[Suppes] p. 104 | Theorem
38 | pwfi 8536 |
[Suppes] p. 105 | Theorem
40 | pwfi 8536 |
[Suppes] p. 111 | Axiom
for cardinal numbers | carden 9695 |
[Suppes] p.
130 | Definition 3 | df-tr 4978 |
[Suppes] p. 132 | Theorem
9 | ssonuni 7252 |
[Suppes] p.
134 | Definition 6 | df-suc 5973 |
[Suppes] p. 136 | Theorem
Schema 22 | findes 7362 finds 7358 finds1 7361 finds2 7360 |
[Suppes] p. 151 | Theorem
42 | isfinite 8833 isfinite2 8493 isfiniteg 8495 unbnn 8491 |
[Suppes] p.
162 | Definition 5 | df-ltnq 10062 df-ltpq 10054 |
[Suppes] p. 197 | Theorem
Schema 4 | tfindes 7328 tfinds 7325 tfinds2 7329 |
[Suppes] p. 209 | Theorem
18 | oaord1 7903 |
[Suppes] p. 209 | Theorem
21 | oaword2 7905 |
[Suppes] p. 211 | Theorem
25 | oaass 7913 |
[Suppes] p.
225 | Definition 8 | iscard2 9122 |
[Suppes] p. 227 | Theorem
56 | ondomon 9707 |
[Suppes] p. 228 | Theorem
59 | harcard 9124 |
[Suppes] p.
228 | Definition 12(i) | aleph0 9209 |
[Suppes] p. 228 | Theorem
Schema 61 | onintss 6017 |
[Suppes] p. 228 | Theorem
Schema 62 | onminesb 7264 onminsb 7265 |
[Suppes] p. 229 | Theorem
64 | alephval2 9716 |
[Suppes] p. 229 | Theorem
65 | alephcard 9213 |
[Suppes] p. 229 | Theorem
66 | alephord2i 9220 |
[Suppes] p. 229 | Theorem
67 | alephnbtwn 9214 |
[Suppes] p.
229 | Definition 12 | df-aleph 9086 |
[Suppes] p. 242 | Theorem
6 | weth 9639 |
[Suppes] p. 242 | Theorem
8 | entric 9701 |
[Suppes] p. 242 | Theorem
9 | carden 9695 |
[TakeutiZaring] p.
8 | Axiom 1 | ax-ext 2803 |
[TakeutiZaring] p.
13 | Definition 4.5 | df-cleq 2818 |
[TakeutiZaring] p.
13 | Proposition 4.6 | df-clel 2821 |
[TakeutiZaring] p.
13 | Proposition 4.9 | cvjust 2820 |
[TakeutiZaring] p.
13 | Proposition 4.7(3) | eqtr 2846 |
[TakeutiZaring] p.
14 | Definition 4.16 | df-oprab 6914 |
[TakeutiZaring] p.
14 | Proposition 4.14 | ru 3661 |
[TakeutiZaring] p.
15 | Axiom 2 | zfpair 5127 |
[TakeutiZaring] p.
15 | Exercise 1 | elpr 4422 elpr2 4423 elprg 4420 |
[TakeutiZaring] p.
15 | Exercise 2 | elsn 4414 elsn2 4434 elsn2g 4433 elsng 4413 velsn 4415 |
[TakeutiZaring] p.
15 | Exercise 3 | elop 5158 |
[TakeutiZaring] p.
15 | Exercise 4 | sneq 4409 sneqr 4589 |
[TakeutiZaring] p.
15 | Definition 5.1 | dfpr2 4418 dfsn2 4412 dfsn2ALT 4419 |
[TakeutiZaring] p.
16 | Axiom 3 | uniex 7218 |
[TakeutiZaring] p.
16 | Exercise 6 | opth 5167 |
[TakeutiZaring] p.
16 | Exercise 7 | opex 5155 |
[TakeutiZaring] p.
16 | Exercise 8 | rext 5139 |
[TakeutiZaring] p.
16 | Corollary 5.8 | unex 7221 unexg 7224 |
[TakeutiZaring] p.
16 | Definition 5.3 | dftp2 4452 |
[TakeutiZaring] p.
16 | Definition 5.5 | df-uni 4661 |
[TakeutiZaring] p.
16 | Definition 5.6 | df-in 3805 df-un 3803 |
[TakeutiZaring] p.
16 | Proposition 5.7 | unipr 4673 uniprg 4674 |
[TakeutiZaring] p.
17 | Axiom 4 | vpwex 5079 |
[TakeutiZaring] p.
17 | Exercise 1 | eltp 4451 |
[TakeutiZaring] p.
17 | Exercise 5 | elsuc 6036 elsucg 6034 sstr2 3834 |
[TakeutiZaring] p.
17 | Exercise 6 | uncom 3986 |
[TakeutiZaring] p.
17 | Exercise 7 | incom 4034 |
[TakeutiZaring] p.
17 | Exercise 8 | unass 3999 |
[TakeutiZaring] p.
17 | Exercise 9 | inass 4050 |
[TakeutiZaring] p.
17 | Exercise 10 | indi 4105 |
[TakeutiZaring] p.
17 | Exercise 11 | undi 4106 |
[TakeutiZaring] p.
17 | Definition 5.9 | df-pss 3814 dfss2 3815 |
[TakeutiZaring] p.
17 | Definition 5.10 | df-pw 4382 |
[TakeutiZaring] p.
18 | Exercise 7 | unss2 4013 |
[TakeutiZaring] p.
18 | Exercise 9 | df-ss 3812 sseqin2 4046 |
[TakeutiZaring] p.
18 | Exercise 10 | ssid 3848 |
[TakeutiZaring] p.
18 | Exercise 12 | inss1 4059 inss2 4060 |
[TakeutiZaring] p.
18 | Exercise 13 | nss 3888 |
[TakeutiZaring] p.
18 | Exercise 15 | unieq 4668 |
[TakeutiZaring] p.
18 | Exercise 18 | sspwb 5140 sspwimp 39967 sspwimpALT 39974 sspwimpALT2 39977 sspwimpcf 39969 |
[TakeutiZaring] p.
18 | Exercise 19 | pweqb 5148 |
[TakeutiZaring] p.
19 | Axiom 5 | ax-rep 4996 |
[TakeutiZaring] p.
20 | Definition | df-rab 3126 |
[TakeutiZaring] p.
20 | Corollary 5.16 | 0ex 5016 |
[TakeutiZaring] p.
20 | Definition 5.12 | df-dif 3801 |
[TakeutiZaring] p.
20 | Definition 5.14 | dfnul2 4148 |
[TakeutiZaring] p.
20 | Proposition 5.15 | difid 4180 |
[TakeutiZaring] p.
20 | Proposition 5.17(1) | n0 4162 n0f 4159
neq0 4161 neq0f 4158 |
[TakeutiZaring] p.
21 | Axiom 6 | zfreg 8776 |
[TakeutiZaring] p.
21 | Axiom 6' | zfregs 8892 |
[TakeutiZaring] p.
21 | Theorem 5.22 | setind 8894 |
[TakeutiZaring] p.
21 | Definition 5.20 | df-v 3416 |
[TakeutiZaring] p.
21 | Proposition 5.21 | vprc 5024 |
[TakeutiZaring] p.
22 | Exercise 1 | 0ss 4199 |
[TakeutiZaring] p.
22 | Exercise 3 | ssex 5029 ssexg 5031 |
[TakeutiZaring] p.
22 | Exercise 4 | inex1 5026 |
[TakeutiZaring] p.
22 | Exercise 5 | ruv 8783 |
[TakeutiZaring] p.
22 | Exercise 6 | elirr 8778 |
[TakeutiZaring] p.
22 | Exercise 7 | ssdif0 4173 |
[TakeutiZaring] p.
22 | Exercise 11 | difdif 3965 |
[TakeutiZaring] p.
22 | Exercise 13 | undif3 4120 undif3VD 39931 |
[TakeutiZaring] p.
22 | Exercise 14 | difss 3966 |
[TakeutiZaring] p.
22 | Exercise 15 | sscon 3973 |
[TakeutiZaring] p.
22 | Definition 4.15(3) | df-ral 3122 |
[TakeutiZaring] p.
22 | Definition 4.15(4) | df-rex 3123 |
[TakeutiZaring] p.
23 | Proposition 6.2 | xpex 7228 xpexg 7225 |
[TakeutiZaring] p.
23 | Definition 6.4(1) | df-rel 5353 |
[TakeutiZaring] p.
23 | Definition 6.4(2) | fun2cnv 6197 |
[TakeutiZaring] p.
24 | Definition 6.4(3) | f1cnvcnv 6351 fun11 6200 |
[TakeutiZaring] p.
24 | Definition 6.4(4) | dffun4 6139 svrelfun 6198 |
[TakeutiZaring] p.
24 | Definition 6.5(1) | dfdm3 5546 |
[TakeutiZaring] p.
24 | Definition 6.5(2) | dfrn3 5548 |
[TakeutiZaring] p.
24 | Definition 6.6(1) | df-res 5358 |
[TakeutiZaring] p.
24 | Definition 6.6(2) | df-ima 5359 |
[TakeutiZaring] p.
24 | Definition 6.6(3) | df-co 5355 |
[TakeutiZaring] p.
25 | Exercise 2 | cnvcnvss 5833 dfrel2 5828 |
[TakeutiZaring] p.
25 | Exercise 3 | xpss 5362 |
[TakeutiZaring] p.
25 | Exercise 5 | relun 5473 |
[TakeutiZaring] p.
25 | Exercise 6 | reluni 5480 |
[TakeutiZaring] p.
25 | Exercise 9 | inxp 5491 |
[TakeutiZaring] p.
25 | Exercise 12 | relres 5666 |
[TakeutiZaring] p.
25 | Exercise 13 | opelres 5639 opelresi 5641 |
[TakeutiZaring] p.
25 | Exercise 14 | dmres 5659 |
[TakeutiZaring] p.
25 | Exercise 15 | resss 5662 |
[TakeutiZaring] p.
25 | Exercise 17 | resabs1 5667 |
[TakeutiZaring] p.
25 | Exercise 18 | funres 6169 |
[TakeutiZaring] p.
25 | Exercise 24 | relco 5878 |
[TakeutiZaring] p.
25 | Exercise 29 | funco 6167 |
[TakeutiZaring] p.
25 | Exercise 30 | f1co 6352 |
[TakeutiZaring] p.
26 | Definition 6.10 | eu2 2694 |
[TakeutiZaring] p.
26 | Definition 6.11 | conventions 27811 df-fv 6135 fv3 6455 |
[TakeutiZaring] p.
26 | Corollary 6.8(1) | cnvex 7380 cnvexg 7379 |
[TakeutiZaring] p.
26 | Corollary 6.8(2) | dmex 7366 dmexg 7363 |
[TakeutiZaring] p.
26 | Corollary 6.8(3) | rnex 7367 rnexg 7364 |
[TakeutiZaring] p. 26 | Corollary
6.9(1) | xpexb 39491 |
[TakeutiZaring] p.
26 | Corollary 6.9(2) | xpexcnv 7375 |
[TakeutiZaring] p.
27 | Corollary 6.13 | fvex 6450 |
[TakeutiZaring] p. 27 | Theorem
6.12(1) | tz6.12-1-afv 42070 tz6.12-1-afv2 42137 tz6.12-1 6459 tz6.12-afv 42069 tz6.12-afv2 42136 tz6.12 6460 tz6.12c-afv2 42138 tz6.12c 6462 |
[TakeutiZaring] p. 27 | Theorem
6.12(2) | tz6.12-2-afv2 42133 tz6.12-2 6427 tz6.12i-afv2 42139 tz6.12i 6463 |
[TakeutiZaring] p.
27 | Definition 6.15(1) | df-fn 6130 |
[TakeutiZaring] p.
27 | Definition 6.15(3) | df-f 6131 |
[TakeutiZaring] p.
27 | Definition 6.15(4) | df-fo 6133 wfo 6125 |
[TakeutiZaring] p.
27 | Definition 6.15(5) | df-f1 6132 wf1 6124 |
[TakeutiZaring] p.
27 | Definition 6.15(6) | df-f1o 6134 wf1o 6126 |
[TakeutiZaring] p.
28 | Exercise 4 | eqfnfv 6565 eqfnfv2 6566 eqfnfv2f 6569 |
[TakeutiZaring] p.
28 | Exercise 5 | fvco 6525 |
[TakeutiZaring] p.
28 | Theorem 6.16(1) | fnex 6742 |
[TakeutiZaring] p.
28 | Proposition 6.17 | resfunexg 6740 |
[TakeutiZaring] p.
29 | Exercise 9 | funimaex 6213 funimaexg 6212 |
[TakeutiZaring] p.
29 | Definition 6.18 | df-br 4876 |
[TakeutiZaring] p.
29 | Definition 6.19(1) | df-so 5266 |
[TakeutiZaring] p.
30 | Definition 6.21 | dffr2 5311 dffr3 5743 eliniseg 5739 iniseg 5741 |
[TakeutiZaring] p.
30 | Definition 6.22 | df-eprel 5257 |
[TakeutiZaring] p.
30 | Proposition 6.23 | fr2nr 5324 fr3nr 7245 frirr 5323 |
[TakeutiZaring] p.
30 | Definition 6.24(1) | df-fr 5305 |
[TakeutiZaring] p.
30 | Definition 6.24(2) | dfwe2 7247 |
[TakeutiZaring] p.
31 | Exercise 1 | frss 5313 |
[TakeutiZaring] p.
31 | Exercise 4 | wess 5333 |
[TakeutiZaring] p.
31 | Proposition 6.26 | tz6.26 5955 tz6.26i 5956 wefrc 5340 wereu2 5343 |
[TakeutiZaring] p.
32 | Theorem 6.27 | wfi 5957 wfii 5958 |
[TakeutiZaring] p.
32 | Definition 6.28 | df-isom 6136 |
[TakeutiZaring] p.
33 | Proposition 6.30(1) | isoid 6839 |
[TakeutiZaring] p.
33 | Proposition 6.30(2) | isocnv 6840 |
[TakeutiZaring] p.
33 | Proposition 6.30(3) | isotr 6846 |
[TakeutiZaring] p.
33 | Proposition 6.31(1) | isomin 6847 |
[TakeutiZaring] p.
33 | Proposition 6.31(2) | isoini 6848 |
[TakeutiZaring] p.
33 | Proposition 6.32(1) | isofr 6852 |
[TakeutiZaring] p.
33 | Proposition 6.32(3) | isowe 6859 |
[TakeutiZaring] p.
34 | Proposition 6.33 | f1oiso 6861 |
[TakeutiZaring] p.
35 | Notation | wtr 4977 |
[TakeutiZaring] p. 35 | Theorem
7.2 | trelpss 39492 tz7.2 5330 |
[TakeutiZaring] p.
35 | Definition 7.1 | dftr3 4981 |
[TakeutiZaring] p.
36 | Proposition 7.4 | ordwe 5980 |
[TakeutiZaring] p.
36 | Proposition 7.5 | tz7.5 5988 |
[TakeutiZaring] p.
36 | Proposition 7.6 | ordelord 5989 ordelordALT 39576 ordelordALTVD 39916 |
[TakeutiZaring] p.
37 | Corollary 7.8 | ordelpss 5995 ordelssne 5994 |
[TakeutiZaring] p.
37 | Proposition 7.7 | tz7.7 5993 |
[TakeutiZaring] p.
37 | Proposition 7.9 | ordin 5997 |
[TakeutiZaring] p.
38 | Corollary 7.14 | ordeleqon 7254 |
[TakeutiZaring] p.
38 | Corollary 7.15 | ordsson 7255 |
[TakeutiZaring] p.
38 | Definition 7.11 | df-on 5971 |
[TakeutiZaring] p.
38 | Proposition 7.10 | ordtri3or 5999 |
[TakeutiZaring] p. 38 | Proposition
7.12 | onfrALT 39588 ordon 7249 |
[TakeutiZaring] p.
38 | Proposition 7.13 | onprc 7250 |
[TakeutiZaring] p.
39 | Theorem 7.17 | tfi 7319 |
[TakeutiZaring] p.
40 | Exercise 3 | ontr2 6014 |
[TakeutiZaring] p.
40 | Exercise 7 | dftr2 4979 |
[TakeutiZaring] p.
40 | Exercise 9 | onssmin 7263 |
[TakeutiZaring] p.
40 | Exercise 11 | unon 7297 |
[TakeutiZaring] p.
40 | Exercise 12 | ordun 6068 |
[TakeutiZaring] p.
40 | Exercise 14 | ordequn 6067 |
[TakeutiZaring] p.
40 | Proposition 7.19 | ssorduni 7251 |
[TakeutiZaring] p.
40 | Proposition 7.20 | elssuni 4691 |
[TakeutiZaring] p.
41 | Definition 7.22 | df-suc 5973 |
[TakeutiZaring] p.
41 | Proposition 7.23 | sssucid 6044 sucidg 6045 |
[TakeutiZaring] p.
41 | Proposition 7.24 | suceloni 7279 |
[TakeutiZaring] p.
41 | Proposition 7.25 | onnbtwn 6058 ordnbtwn 6057 |
[TakeutiZaring] p.
41 | Proposition 7.26 | onsucuni 7294 |
[TakeutiZaring] p.
42 | Exercise 1 | df-lim 5972 |
[TakeutiZaring] p.
42 | Exercise 4 | omssnlim 7345 |
[TakeutiZaring] p.
42 | Exercise 7 | ssnlim 7349 |
[TakeutiZaring] p.
42 | Exercise 8 | onsucssi 7307 ordelsuc 7286 |
[TakeutiZaring] p.
42 | Exercise 9 | ordsucelsuc 7288 |
[TakeutiZaring] p.
42 | Definition 7.27 | nlimon 7317 |
[TakeutiZaring] p.
42 | Definition 7.28 | dfom2 7333 |
[TakeutiZaring] p.
42 | Proposition 7.30(1) | peano1 7351 |
[TakeutiZaring] p.
42 | Proposition 7.30(2) | peano2 7352 |
[TakeutiZaring] p.
42 | Proposition 7.30(3) | peano3 7353 |
[TakeutiZaring] p.
43 | Remark | omon 7342 |
[TakeutiZaring] p.
43 | Axiom 7 | inf3 8816 omex 8824 |
[TakeutiZaring] p.
43 | Theorem 7.32 | ordom 7340 |
[TakeutiZaring] p.
43 | Corollary 7.31 | find 7357 |
[TakeutiZaring] p.
43 | Proposition 7.30(4) | peano4 7354 |
[TakeutiZaring] p.
43 | Proposition 7.30(5) | peano5 7355 |
[TakeutiZaring] p.
44 | Exercise 1 | limomss 7336 |
[TakeutiZaring] p.
44 | Exercise 2 | int0 4713 |
[TakeutiZaring] p.
44 | Exercise 3 | trintss 4995 |
[TakeutiZaring] p.
44 | Exercise 4 | intss1 4714 |
[TakeutiZaring] p.
44 | Exercise 5 | intex 5044 |
[TakeutiZaring] p.
44 | Exercise 6 | oninton 7266 |
[TakeutiZaring] p.
44 | Exercise 11 | ordintdif 6016 |
[TakeutiZaring] p.
44 | Definition 7.35 | df-int 4700 |
[TakeutiZaring] p.
44 | Proposition 7.34 | noinfep 8841 |
[TakeutiZaring] p.
45 | Exercise 4 | onint 7261 |
[TakeutiZaring] p.
47 | Lemma 1 | tfrlem1 7743 |
[TakeutiZaring] p.
47 | Theorem 7.41(1) | tfr1 7764 |
[TakeutiZaring] p.
47 | Theorem 7.41(2) | tfr2 7765 |
[TakeutiZaring] p.
47 | Theorem 7.41(3) | tfr3 7766 |
[TakeutiZaring] p.
49 | Theorem 7.44 | tz7.44-1 7773 tz7.44-2 7774 tz7.44-3 7775 |
[TakeutiZaring] p.
50 | Exercise 1 | smogt 7735 |
[TakeutiZaring] p.
50 | Exercise 3 | smoiso 7730 |
[TakeutiZaring] p.
50 | Definition 7.46 | df-smo 7714 |
[TakeutiZaring] p.
51 | Proposition 7.49 | tz7.49 7811 tz7.49c 7812 |
[TakeutiZaring] p.
51 | Proposition 7.48(1) | tz7.48-1 7809 |
[TakeutiZaring] p.
51 | Proposition 7.48(2) | tz7.48-2 7808 |
[TakeutiZaring] p.
51 | Proposition 7.48(3) | tz7.48-3 7810 |
[TakeutiZaring] p.
53 | Proposition 7.53 | 2eu5 2737 |
[TakeutiZaring] p.
54 | Proposition 7.56(1) | leweon 9154 |
[TakeutiZaring] p.
54 | Proposition 7.58(1) | r0weon 9155 |
[TakeutiZaring] p.
56 | Definition 8.1 | oalim 7884 oasuc 7876 |
[TakeutiZaring] p.
57 | Remark | tfindsg 7326 |
[TakeutiZaring] p.
57 | Proposition 8.2 | oacl 7887 |
[TakeutiZaring] p.
57 | Proposition 8.3 | oa0 7868 oa0r 7890 |
[TakeutiZaring] p.
57 | Proposition 8.16 | omcl 7888 |
[TakeutiZaring] p.
58 | Corollary 8.5 | oacan 7900 |
[TakeutiZaring] p.
58 | Proposition 8.4 | nnaord 7971 nnaordi 7970 oaord 7899 oaordi 7898 |
[TakeutiZaring] p.
59 | Proposition 8.6 | iunss2 4787 uniss2 4694 |
[TakeutiZaring] p.
59 | Proposition 8.7 | oawordri 7902 |
[TakeutiZaring] p.
59 | Proposition 8.8 | oawordeu 7907 oawordex 7909 |
[TakeutiZaring] p.
59 | Proposition 8.9 | nnacl 7963 |
[TakeutiZaring] p.
59 | Proposition 8.10 | oaabs 7996 |
[TakeutiZaring] p.
60 | Remark | oancom 8832 |
[TakeutiZaring] p.
60 | Proposition 8.11 | oalimcl 7912 |
[TakeutiZaring] p.
62 | Exercise 1 | nnarcl 7968 |
[TakeutiZaring] p.
62 | Exercise 5 | oaword1 7904 |
[TakeutiZaring] p.
62 | Definition 8.15 | om0x 7871 omlim 7885 omsuc 7878 |
[TakeutiZaring] p.
62 | Definition 8.15(a) | om0 7869 |
[TakeutiZaring] p.
63 | Proposition 8.17 | nnecl 7965 nnmcl 7964 |
[TakeutiZaring] p.
63 | Proposition 8.19 | nnmord 7984 nnmordi 7983 omord 7920 omordi 7918 |
[TakeutiZaring] p.
63 | Proposition 8.20 | omcan 7921 |
[TakeutiZaring] p.
63 | Proposition 8.21 | nnmwordri 7988 omwordri 7924 |
[TakeutiZaring] p.
63 | Proposition 8.18(1) | om0r 7891 |
[TakeutiZaring] p.
63 | Proposition 8.18(2) | om1 7894 om1r 7895 |
[TakeutiZaring] p.
64 | Proposition 8.22 | om00 7927 |
[TakeutiZaring] p.
64 | Proposition 8.23 | omordlim 7929 |
[TakeutiZaring] p.
64 | Proposition 8.24 | omlimcl 7930 |
[TakeutiZaring] p.
64 | Proposition 8.25 | odi 7931 |
[TakeutiZaring] p.
65 | Theorem 8.26 | omass 7932 |
[TakeutiZaring] p.
67 | Definition 8.30 | nnesuc 7960 oe0 7874
oelim 7886 oesuc 7879 onesuc 7882 |
[TakeutiZaring] p.
67 | Proposition 8.31 | oe0m0 7872 |
[TakeutiZaring] p.
67 | Proposition 8.32 | oen0 7938 |
[TakeutiZaring] p.
67 | Proposition 8.33 | oeordi 7939 |
[TakeutiZaring] p.
67 | Proposition 8.31(2) | oe0m1 7873 |
[TakeutiZaring] p.
67 | Proposition 8.31(3) | oe1m 7897 |
[TakeutiZaring] p.
68 | Corollary 8.34 | oeord 7940 |
[TakeutiZaring] p.
68 | Corollary 8.36 | oeordsuc 7946 |
[TakeutiZaring] p.
68 | Proposition 8.35 | oewordri 7944 |
[TakeutiZaring] p.
68 | Proposition 8.37 | oeworde 7945 |
[TakeutiZaring] p.
69 | Proposition 8.41 | oeoa 7949 |
[TakeutiZaring] p.
70 | Proposition 8.42 | oeoe 7951 |
[TakeutiZaring] p.
73 | Theorem 9.1 | trcl 8888 tz9.1 8889 |
[TakeutiZaring] p.
76 | Definition 9.9 | df-r1 8911 r10 8915
r1lim 8919 r1limg 8918 r1suc 8917 r1sucg 8916 |
[TakeutiZaring] p.
77 | Proposition 9.10(2) | r1ord 8927 r1ord2 8928 r1ordg 8925 |
[TakeutiZaring] p.
78 | Proposition 9.12 | tz9.12 8937 |
[TakeutiZaring] p.
78 | Proposition 9.13 | rankwflem 8962 tz9.13 8938 tz9.13g 8939 |
[TakeutiZaring] p.
79 | Definition 9.14 | df-rank 8912 rankval 8963 rankvalb 8944 rankvalg 8964 |
[TakeutiZaring] p.
79 | Proposition 9.16 | rankel 8986 rankelb 8971 |
[TakeutiZaring] p.
79 | Proposition 9.17 | rankuni2b 9000 rankval3 8987 rankval3b 8973 |
[TakeutiZaring] p.
79 | Proposition 9.18 | rankonid 8976 |
[TakeutiZaring] p.
79 | Proposition 9.15(1) | rankon 8942 |
[TakeutiZaring] p.
79 | Proposition 9.15(2) | rankr1 8981 rankr1c 8968 rankr1g 8979 |
[TakeutiZaring] p.
79 | Proposition 9.15(3) | ssrankr1 8982 |
[TakeutiZaring] p.
80 | Exercise 1 | rankss 8996 rankssb 8995 |
[TakeutiZaring] p.
80 | Exercise 2 | unbndrank 8989 |
[TakeutiZaring] p.
80 | Proposition 9.19 | bndrank 8988 |
[TakeutiZaring] p.
83 | Axiom of Choice | ac4 9619 dfac3 9264 |
[TakeutiZaring] p.
84 | Theorem 10.3 | dfac8a 9173 numth 9616 numth2 9615 |
[TakeutiZaring] p.
85 | Definition 10.4 | cardval 9690 |
[TakeutiZaring] p.
85 | Proposition 10.5 | cardid 9691 cardid2 9099 |
[TakeutiZaring] p.
85 | Proposition 10.9 | oncard 9106 |
[TakeutiZaring] p.
85 | Proposition 10.10 | carden 9695 |
[TakeutiZaring] p.
85 | Proposition 10.11 | cardidm 9105 |
[TakeutiZaring] p.
85 | Proposition 10.6(1) | cardon 9090 |
[TakeutiZaring] p.
85 | Proposition 10.6(2) | cardne 9111 |
[TakeutiZaring] p.
85 | Proposition 10.6(3) | cardonle 9103 |
[TakeutiZaring] p.
87 | Proposition 10.15 | pwen 8408 |
[TakeutiZaring] p.
88 | Exercise 1 | en0 8291 |
[TakeutiZaring] p.
88 | Exercise 7 | infensuc 8413 |
[TakeutiZaring] p.
89 | Exercise 10 | omxpen 8337 |
[TakeutiZaring] p.
90 | Corollary 10.23 | cardnn 9109 |
[TakeutiZaring] p.
90 | Definition 10.27 | alephiso 9241 |
[TakeutiZaring] p.
90 | Proposition 10.20 | nneneq 8418 |
[TakeutiZaring] p.
90 | Proposition 10.22 | onomeneq 8425 |
[TakeutiZaring] p.
90 | Proposition 10.26 | alephprc 9242 |
[TakeutiZaring] p.
90 | Corollary 10.21(1) | php5 8423 |
[TakeutiZaring] p.
91 | Exercise 2 | alephle 9231 |
[TakeutiZaring] p.
91 | Exercise 3 | aleph0 9209 |
[TakeutiZaring] p.
91 | Exercise 4 | cardlim 9118 |
[TakeutiZaring] p.
91 | Exercise 7 | infpss 9361 |
[TakeutiZaring] p.
91 | Exercise 8 | infcntss 8509 |
[TakeutiZaring] p.
91 | Definition 10.29 | df-fin 8232 isfi 8252 |
[TakeutiZaring] p.
92 | Proposition 10.32 | onfin 8426 |
[TakeutiZaring] p.
92 | Proposition 10.34 | imadomg 9678 |
[TakeutiZaring] p.
92 | Proposition 10.33(2) | xpdom2 8330 |
[TakeutiZaring] p.
93 | Proposition 10.35 | fodomb 9670 |
[TakeutiZaring] p.
93 | Proposition 10.36 | cdaxpdom 9333 unxpdom 8442 |
[TakeutiZaring] p.
93 | Proposition 10.37 | cardsdomel 9120 cardsdomelir 9119 |
[TakeutiZaring] p.
93 | Proposition 10.38 | sucxpdom 8444 |
[TakeutiZaring] p.
94 | Proposition 10.39 | infxpen 9157 |
[TakeutiZaring] p.
95 | Definition 10.42 | df-map 8129 |
[TakeutiZaring] p.
95 | Proposition 10.40 | infxpidm 9706 infxpidm2 9160 |
[TakeutiZaring] p.
95 | Proposition 10.41 | infcda 9352 infxp 9359 |
[TakeutiZaring] p.
96 | Proposition 10.44 | pw2en 8342 pw2f1o 8340 |
[TakeutiZaring] p.
96 | Proposition 10.45 | mapxpen 8401 |
[TakeutiZaring] p.
97 | Theorem 10.46 | ac6s3 9631 |
[TakeutiZaring] p.
98 | Theorem 10.46 | ac6c5 9626 ac6s5 9635 |
[TakeutiZaring] p.
98 | Theorem 10.47 | unidom 9687 |
[TakeutiZaring] p.
99 | Theorem 10.48 | uniimadom 9688 uniimadomf 9689 |
[TakeutiZaring] p.
100 | Definition 11.1 | cfcof 9418 |
[TakeutiZaring] p.
101 | Proposition 11.7 | cofsmo 9413 |
[TakeutiZaring] p.
102 | Exercise 1 | cfle 9398 |
[TakeutiZaring] p.
102 | Exercise 2 | cf0 9395 |
[TakeutiZaring] p.
102 | Exercise 3 | cfsuc 9401 |
[TakeutiZaring] p.
102 | Exercise 4 | cfom 9408 |
[TakeutiZaring] p.
102 | Proposition 11.9 | coftr 9417 |
[TakeutiZaring] p.
103 | Theorem 11.15 | alephreg 9726 |
[TakeutiZaring] p.
103 | Proposition 11.11 | cardcf 9396 |
[TakeutiZaring] p.
103 | Proposition 11.13 | alephsing 9420 |
[TakeutiZaring] p.
104 | Corollary 11.17 | cardinfima 9240 |
[TakeutiZaring] p.
104 | Proposition 11.16 | carduniima 9239 |
[TakeutiZaring] p.
104 | Proposition 11.18 | alephfp 9251 alephfp2 9252 |
[TakeutiZaring] p.
106 | Theorem 11.20 | gchina 9843 |
[TakeutiZaring] p.
106 | Theorem 11.21 | mappwen 9255 |
[TakeutiZaring] p.
107 | Theorem 11.26 | konigth 9713 |
[TakeutiZaring] p.
108 | Theorem 11.28 | pwcfsdom 9727 |
[TakeutiZaring] p.
108 | Theorem 11.29 | cfpwsdom 9728 |
[Tarski] p.
67 | Axiom B5 | ax-c5 34953 |
[Tarski] p. 67 | Scheme
B5 | sp 2224 |
[Tarski] p. 68 | Lemma
6 | avril1 27873 equid 2116 |
[Tarski] p. 69 | Lemma
7 | equcomi 2121 |
[Tarski] p. 70 | Lemma
14 | spim 2407 spime 2409 spimeh 2101 |
[Tarski] p. 70 | Lemma
16 | ax-12 2220 ax-c15 34959 ax12i 2066 |
[Tarski] p. 70 | Lemmas 16
and 17 | sb6 2307 |
[Tarski] p. 75 | Axiom
B7 | ax6v 2076 |
[Tarski] p. 77 | Axiom B6
(p. 75) of system S2 | ax-5 2009 ax5ALT 34977 |
[Tarski], p. 75 | Scheme
B8 of system S2 | ax-7 2112 ax-8 2166
ax-9 2173 |
[Tarski1999] p.
178 | Axiom 4 | axtgsegcon 25783 |
[Tarski1999] p.
178 | Axiom 5 | axtg5seg 25784 |
[Tarski1999] p.
179 | Axiom 7 | axtgpasch 25786 |
[Tarski1999] p.
180 | Axiom 7.1 | axtgpasch 25786 |
[Tarski1999] p.
185 | Axiom 11 | axtgcont1 25787 |
[Truss] p. 114 | Theorem
5.18 | ruc 15353 |
[Viaclovsky7] p. 3 | Corollary
0.3 | mblfinlem3 33987 |
[Viaclovsky8] p. 3 | Proposition
7 | ismblfin 33989 |
[Weierstrass] p.
272 | Definition | df-mdet 20766 mdetuni 20803 |
[WhiteheadRussell] p.
96 | Axiom *1.2 | pm1.2 932 |
[WhiteheadRussell] p.
96 | Axiom *1.3 | olc 899 |
[WhiteheadRussell] p.
96 | Axiom *1.4 | pm1.4 900 |
[WhiteheadRussell] p.
96 | Axiom *1.5 (Assoc) | pm1.5 948 |
[WhiteheadRussell] p.
97 | Axiom *1.6 (Sum) | orim2 995 |
[WhiteheadRussell] p.
100 | Theorem *2.01 | pm2.01 181 |
[WhiteheadRussell] p.
100 | Theorem *2.02 | ax-1 6 |
[WhiteheadRussell] p.
100 | Theorem *2.03 | con2 133 |
[WhiteheadRussell] p.
100 | Theorem *2.04 | pm2.04 90 wl-luk-pm2.04 33809 |
[WhiteheadRussell] p.
100 | Theorem *2.05 | frege5 38929 imim2 58
wl-luk-imim2 33804 |
[WhiteheadRussell] p.
100 | Theorem *2.06 | imim1 83 |
[WhiteheadRussell] p.
101 | Theorem *2.1 | pm2.1 925 |
[WhiteheadRussell] p.
101 | Theorem *2.06 | barbara 2746 syl 17 |
[WhiteheadRussell] p.
101 | Theorem *2.07 | pm2.07 931 |
[WhiteheadRussell] p.
101 | Theorem *2.08 | id 22 wl-luk-id 33807 |
[WhiteheadRussell] p.
101 | Theorem *2.11 | exmid 923 |
[WhiteheadRussell] p.
101 | Theorem *2.12 | notnot 139 |
[WhiteheadRussell] p.
101 | Theorem *2.13 | pm2.13 926 |
[WhiteheadRussell] p.
102 | Theorem *2.14 | notnotr 128 notnotrALT2 39976 wl-luk-notnotr 33808 |
[WhiteheadRussell] p.
102 | Theorem *2.15 | con1 146 |
[WhiteheadRussell] p.
103 | Theorem *2.16 | ax-frege28 38959 axfrege28 38958 con3 151 |
[WhiteheadRussell] p.
103 | Theorem *2.17 | ax-3 8 |
[WhiteheadRussell] p.
103 | Theorem *2.18 | pm2.18 125 |
[WhiteheadRussell] p.
104 | Theorem *2.2 | orc 898 |
[WhiteheadRussell] p.
104 | Theorem *2.3 | pm2.3 953 |
[WhiteheadRussell] p.
104 | Theorem *2.21 | pm2.21 121 wl-luk-pm2.21 33801 |
[WhiteheadRussell] p.
104 | Theorem *2.24 | pm2.24 122 |
[WhiteheadRussell] p.
104 | Theorem *2.25 | pm2.25 918 |
[WhiteheadRussell] p.
104 | Theorem *2.26 | pm2.26 968 |
[WhiteheadRussell] p.
104 | Theorem *2.27 | conventions-labels 27812 pm2.27 42 wl-luk-pm2.27 33799 |
[WhiteheadRussell] p.
104 | Theorem *2.31 | pm2.31 951 |
[WhiteheadRussell] p.
105 | Theorem *2.32 | pm2.32 952 |
[WhiteheadRussell] p.
105 | Theorem *2.36 | pm2.36 997 |
[WhiteheadRussell] p.
105 | Theorem *2.37 | pm2.37 998 |
[WhiteheadRussell] p.
105 | Theorem *2.38 | pm2.38 996 |
[WhiteheadRussell] p.
105 | Definition *2.33 | df-3or 1112 |
[WhiteheadRussell] p.
106 | Theorem *2.4 | pm2.4 935 |
[WhiteheadRussell] p.
106 | Theorem *2.41 | pm2.41 936 |
[WhiteheadRussell] p.
106 | Theorem *2.42 | pm2.42 971 |
[WhiteheadRussell] p.
106 | Theorem *2.43 | pm2.43 56 |
[WhiteheadRussell] p.
106 | Theorem *2.45 | pm2.45 910 |
[WhiteheadRussell] p.
106 | Theorem *2.46 | pm2.46 911 |
[WhiteheadRussell] p.
107 | Theorem *2.5 | pm2.5 166 |
[WhiteheadRussell] p.
107 | Theorem *2.6 | pm2.6 183 |
[WhiteheadRussell] p.
107 | Theorem *2.47 | pm2.47 912 |
[WhiteheadRussell] p.
107 | Theorem *2.48 | pm2.48 913 |
[WhiteheadRussell] p.
107 | Theorem *2.49 | pm2.49 914 |
[WhiteheadRussell] p.
107 | Theorem *2.51 | pm2.51 167 |
[WhiteheadRussell] p.
107 | Theorem *2.52 | pm2.52 169 |
[WhiteheadRussell] p.
107 | Theorem *2.53 | pm2.53 882 |
[WhiteheadRussell] p.
107 | Theorem *2.54 | pm2.54 883 |
[WhiteheadRussell] p.
107 | Theorem *2.55 | orel1 917 |
[WhiteheadRussell] p.
107 | Theorem *2.56 | orel2 919 |
[WhiteheadRussell] p.
107 | Theorem *2.61 | pm2.61 184 |
[WhiteheadRussell] p.
107 | Theorem *2.62 | pm2.62 928 |
[WhiteheadRussell] p.
107 | Theorem *2.63 | pm2.63 969 |
[WhiteheadRussell] p.
107 | Theorem *2.64 | pm2.64 970 |
[WhiteheadRussell] p.
107 | Theorem *2.65 | pm2.65 185 |
[WhiteheadRussell] p.
107 | Theorem *2.67 | pm2.67-2 920 pm2.67 921 |
[WhiteheadRussell] p.
107 | Theorem *2.521 | pm2.521 168 |
[WhiteheadRussell] p.
107 | Theorem *2.621 | pm2.621 927 |
[WhiteheadRussell] p.
108 | Theorem *2.8 | pm2.8 1000 |
[WhiteheadRussell] p.
108 | Theorem *2.68 | pm2.68 929 |
[WhiteheadRussell] p.
108 | Theorem *2.69 | looinv 195 |
[WhiteheadRussell] p.
108 | Theorem *2.73 | pm2.73 1001 |
[WhiteheadRussell] p.
108 | Theorem *2.74 | pm2.74 1002 |
[WhiteheadRussell] p.
108 | Theorem *2.75 | pm2.75 962 |
[WhiteheadRussell] p.
108 | Theorem *2.76 | pm2.76 960 |
[WhiteheadRussell] p.
108 | Theorem *2.77 | ax-2 7 |
[WhiteheadRussell] p.
108 | Theorem *2.81 | pm2.81 999 |
[WhiteheadRussell] p.
108 | Theorem *2.82 | pm2.82 1003 |
[WhiteheadRussell] p.
108 | Theorem *2.83 | pm2.83 84 |
[WhiteheadRussell] p.
108 | Theorem *2.85 | pm2.85 961 |
[WhiteheadRussell] p.
108 | Theorem *2.86 | pm2.86 109 |
[WhiteheadRussell] p.
111 | Theorem *3.1 | pm3.1 1019 |
[WhiteheadRussell] p.
111 | Theorem *3.2 | pm3.2 463 pm3.2im 159 |
[WhiteheadRussell] p.
111 | Theorem *3.11 | pm3.11 1020 |
[WhiteheadRussell] p.
111 | Theorem *3.12 | pm3.12 1021 |
[WhiteheadRussell] p.
111 | Theorem *3.13 | pm3.13 1022 |
[WhiteheadRussell] p.
111 | Theorem *3.14 | pm3.14 1023 |
[WhiteheadRussell] p.
111 | Theorem *3.21 | pm3.21 465 |
[WhiteheadRussell] p.
111 | Theorem *3.22 | pm3.22 453 |
[WhiteheadRussell] p.
111 | Theorem *3.24 | pm3.24 393 |
[WhiteheadRussell] p.
112 | Theorem *3.35 | pm3.35 837 |
[WhiteheadRussell] p.
112 | Theorem *3.3 (Exp) | pm3.3 441 |
[WhiteheadRussell] p.
112 | Theorem *3.31 (Imp) | pm3.31 442 |
[WhiteheadRussell] p.
112 | Theorem *3.26 (Simp) | simpl 476 simplim 165 |
[WhiteheadRussell] p.
112 | Theorem *3.27 (Simp) | simpr 479 simprim 164 |
[WhiteheadRussell] p.
112 | Theorem *3.33 (Syll) | pm3.33 781 |
[WhiteheadRussell] p.
112 | Theorem *3.34 (Syll) | pm3.34 782 |
[WhiteheadRussell] p.
112 | Theorem *3.37 (Transp) | pm3.37 842 |
[WhiteheadRussell] p.
113 | Fact) | pm3.45 615 |
[WhiteheadRussell] p.
113 | Theorem *3.4 | pm3.4 844 |
[WhiteheadRussell] p.
113 | Theorem *3.41 | pm3.41 488 |
[WhiteheadRussell] p.
113 | Theorem *3.42 | pm3.42 489 |
[WhiteheadRussell] p.
113 | Theorem *3.44 | jao 988 pm3.44 987 |
[WhiteheadRussell] p.
113 | Theorem *3.47 | prth 843 |
[WhiteheadRussell] p.
113 | Theorem *3.43 (Comp) | pm3.43 467 |
[WhiteheadRussell] p.
114 | Theorem *3.48 | pm3.48 991 |
[WhiteheadRussell] p.
116 | Theorem *4.1 | con34b 308 |
[WhiteheadRussell] p.
117 | Theorem *4.2 | biid 253 |
[WhiteheadRussell] p.
117 | Theorem *4.11 | notbi 311 |
[WhiteheadRussell] p.
117 | Theorem *4.12 | con2bi 345 |
[WhiteheadRussell] p.
117 | Theorem *4.13 | notnotb 307 |
[WhiteheadRussell] p.
117 | Theorem *4.14 | pm4.14 841 |
[WhiteheadRussell] p.
117 | Theorem *4.15 | pm4.15 866 |
[WhiteheadRussell] p.
117 | Theorem *4.21 | bicom 214 |
[WhiteheadRussell] p.
117 | Theorem *4.22 | biantr 840 bitr 839 |
[WhiteheadRussell] p.
117 | Theorem *4.24 | pm4.24 559 |
[WhiteheadRussell] p.
117 | Theorem *4.25 | oridm 933 pm4.25 934 |
[WhiteheadRussell] p.
118 | Theorem *4.3 | ancom 454 |
[WhiteheadRussell] p.
118 | Theorem *4.4 | andi 1035 |
[WhiteheadRussell] p.
118 | Theorem *4.31 | orcom 901 |
[WhiteheadRussell] p.
118 | Theorem *4.32 | anass 462 |
[WhiteheadRussell] p.
118 | Theorem *4.33 | orass 950 |
[WhiteheadRussell] p.
118 | Theorem *4.36 | anbi1 625 |
[WhiteheadRussell] p.
118 | Theorem *4.37 | orbi1 946 |
[WhiteheadRussell] p.
118 | Theorem *4.38 | pm4.38 628 |
[WhiteheadRussell] p.
118 | Theorem *4.39 | pm4.39 1004 |
[WhiteheadRussell] p.
118 | Definition *4.34 | df-3an 1113 |
[WhiteheadRussell] p.
119 | Theorem *4.41 | ordi 1033 |
[WhiteheadRussell] p.
119 | Theorem *4.42 | pm4.42 1080 |
[WhiteheadRussell] p.
119 | Theorem *4.43 | pm4.43 1051 |
[WhiteheadRussell] p.
119 | Theorem *4.44 | pm4.44 1024 |
[WhiteheadRussell] p.
119 | Theorem *4.45 | orabs 1026 pm4.45 1025 pm4.45im 863 |
[WhiteheadRussell] p.
120 | Theorem *4.5 | anor 1010 |
[WhiteheadRussell] p.
120 | Theorem *4.6 | imor 884 |
[WhiteheadRussell] p.
120 | Theorem *4.7 | anclb 541 |
[WhiteheadRussell] p.
120 | Theorem *4.51 | ianor 1009 |
[WhiteheadRussell] p.
120 | Theorem *4.52 | pm4.52 1012 |
[WhiteheadRussell] p.
120 | Theorem *4.53 | pm4.53 1013 |
[WhiteheadRussell] p.
120 | Theorem *4.54 | pm4.54 1014 |
[WhiteheadRussell] p.
120 | Theorem *4.55 | pm4.55 1015 |
[WhiteheadRussell] p.
120 | Theorem *4.56 | ioran 1011 pm4.56 1016 |
[WhiteheadRussell] p.
120 | Theorem *4.57 | oran 1017 pm4.57 1018 |
[WhiteheadRussell] p.
120 | Theorem *4.61 | pm4.61 395 |
[WhiteheadRussell] p.
120 | Theorem *4.62 | pm4.62 887 |
[WhiteheadRussell] p.
120 | Theorem *4.63 | pm4.63 388 |
[WhiteheadRussell] p.
120 | Theorem *4.64 | pm4.64 880 |
[WhiteheadRussell] p.
120 | Theorem *4.65 | pm4.65 396 |
[WhiteheadRussell] p.
120 | Theorem *4.66 | pm4.66 881 |
[WhiteheadRussell] p.
120 | Theorem *4.67 | pm4.67 389 |
[WhiteheadRussell] p.
120 | Theorem *4.71 | pm4.71 553 pm4.71d 557 pm4.71i 555 pm4.71r 554 pm4.71rd 558 pm4.71ri 556 |
[WhiteheadRussell] p.
121 | Theorem *4.72 | pm4.72 977 |
[WhiteheadRussell] p.
121 | Theorem *4.73 | iba 523 |
[WhiteheadRussell] p.
121 | Theorem *4.74 | biorf 965 |
[WhiteheadRussell] p.
121 | Theorem *4.76 | jcab 513 pm4.76 514 |
[WhiteheadRussell] p.
121 | Theorem *4.77 | jaob 989 pm4.77 990 |
[WhiteheadRussell] p.
121 | Theorem *4.78 | pm4.78 963 |
[WhiteheadRussell] p.
121 | Theorem *4.79 | pm4.79 1031 |
[WhiteheadRussell] p.
122 | Theorem *4.8 | pm4.8 383 |
[WhiteheadRussell] p.
122 | Theorem *4.81 | pm4.81 384 |
[WhiteheadRussell] p.
122 | Theorem *4.82 | pm4.82 1052 |
[WhiteheadRussell] p.
122 | Theorem *4.83 | pm4.83 1053 |
[WhiteheadRussell] p.
122 | Theorem *4.84 | imbi1 339 |
[WhiteheadRussell] p.
122 | Theorem *4.85 | imbi2 340 |
[WhiteheadRussell] p.
122 | Theorem *4.86 | bibi1 343 |
[WhiteheadRussell] p.
122 | Theorem *4.87 | bi2.04 379 impexp 443 pm4.87 874 |
[WhiteheadRussell] p.
123 | Theorem *5.1 | pm5.1 859 |
[WhiteheadRussell] p.
123 | Theorem *5.11 | pm5.11 972 |
[WhiteheadRussell] p.
123 | Theorem *5.12 | pm5.12 973 |
[WhiteheadRussell] p.
123 | Theorem *5.13 | pm5.13 975 |
[WhiteheadRussell] p.
123 | Theorem *5.14 | pm5.14 974 |
[WhiteheadRussell] p.
124 | Theorem *5.15 | pm5.15 1041 |
[WhiteheadRussell] p.
124 | Theorem *5.16 | pm5.16 1042 |
[WhiteheadRussell] p.
124 | Theorem *5.17 | pm5.17 1040 |
[WhiteheadRussell] p.
124 | Theorem *5.18 | nbbn 375 pm5.18 373 |
[WhiteheadRussell] p.
124 | Theorem *5.19 | pm5.19 378 |
[WhiteheadRussell] p.
124 | Theorem *5.21 | pm5.21 860 |
[WhiteheadRussell] p.
124 | Theorem *5.22 | xor 1043 |
[WhiteheadRussell] p.
124 | Theorem *5.23 | dfbi3 1076 |
[WhiteheadRussell] p.
124 | Theorem *5.24 | pm5.24 1077 |
[WhiteheadRussell] p.
124 | Theorem *5.25 | dfor2 930 |
[WhiteheadRussell] p.
125 | Theorem *5.3 | pm5.3 568 |
[WhiteheadRussell] p.
125 | Theorem *5.4 | pm5.4 380 |
[WhiteheadRussell] p.
125 | Theorem *5.5 | pm5.5 353 |
[WhiteheadRussell] p.
125 | Theorem *5.6 | pm5.6 1029 |
[WhiteheadRussell] p.
125 | Theorem *5.7 | pm5.7 981 |
[WhiteheadRussell] p.
125 | Theorem *5.31 | pm5.31 865 |
[WhiteheadRussell] p.
125 | Theorem *5.32 | pm5.32 569 |
[WhiteheadRussell] p.
125 | Theorem *5.33 | pm5.33 869 |
[WhiteheadRussell] p.
125 | Theorem *5.35 | pm5.35 861 |
[WhiteheadRussell] p.
125 | Theorem *5.36 | pm5.36 867 |
[WhiteheadRussell] p.
125 | Theorem *5.41 | imdi 381 pm5.41 382 |
[WhiteheadRussell] p.
125 | Theorem *5.42 | pm5.42 539 |
[WhiteheadRussell] p.
125 | Theorem *5.44 | pm5.44 538 |
[WhiteheadRussell] p.
125 | Theorem *5.53 | pm5.53 1032 |
[WhiteheadRussell] p.
125 | Theorem *5.54 | pm5.54 1046 |
[WhiteheadRussell] p.
125 | Theorem *5.55 | pm5.55 976 |
[WhiteheadRussell] p.
125 | Theorem *5.61 | pm5.61 1028 |
[WhiteheadRussell] p.
125 | Theorem *5.62 | pm5.62 1047 |
[WhiteheadRussell] p.
125 | Theorem *5.63 | pm5.63 1048 |
[WhiteheadRussell] p.
125 | Theorem *5.71 | pm5.71 1056 |
[WhiteheadRussell] p.
125 | Theorem *5.501 | pm5.501 358 |
[WhiteheadRussell] p.
126 | Theorem *5.74 | pm5.74 262 |
[WhiteheadRussell] p.
126 | Theorem *5.75 | pm5.75 1057 |
[WhiteheadRussell] p.
146 | Theorem *10.12 | pm10.12 39392 |
[WhiteheadRussell] p.
146 | Theorem *10.14 | pm10.14 39393 |
[WhiteheadRussell] p.
147 | Theorem *10.22 | 19.26 1972 |
[WhiteheadRussell] p.
149 | Theorem *10.251 | pm10.251 39394 |
[WhiteheadRussell] p.
149 | Theorem *10.252 | pm10.252 39395 |
[WhiteheadRussell] p.
149 | Theorem *10.253 | pm10.253 39396 |
[WhiteheadRussell] p.
150 | Theorem *10.3 | alsyl 1995 |
[WhiteheadRussell] p.
151 | Theorem *10.301 | albitr 39397 |
[WhiteheadRussell] p.
155 | Theorem *10.42 | pm10.42 39398 |
[WhiteheadRussell] p.
155 | Theorem *10.52 | pm10.52 39399 |
[WhiteheadRussell] p.
155 | Theorem *10.53 | pm10.53 39400 |
[WhiteheadRussell] p.
155 | Theorem *10.541 | pm10.541 39401 |
[WhiteheadRussell] p.
156 | Theorem *10.55 | pm10.55 39403 |
[WhiteheadRussell] p.
156 | Theorem *10.56 | pm10.56 39404 |
[WhiteheadRussell] p.
156 | Theorem *10.57 | pm10.57 39405 |
[WhiteheadRussell] p.
156 | Theorem *10.542 | pm10.542 39402 |
[WhiteheadRussell] p.
159 | Axiom *11.07 | pm11.07 2581 |
[WhiteheadRussell] p.
159 | Theorem *11.11 | pm11.11 39408 |
[WhiteheadRussell] p.
159 | Theorem *11.12 | pm11.12 39409 |
[WhiteheadRussell] p.
159 | Theorem PM*11.1 | 2stdpc4 2484 |
[WhiteheadRussell] p.
160 | Theorem *11.21 | alrot3 2210 |
[WhiteheadRussell] p.
160 | Theorem *11.22 | 2exnaln 1927 |
[WhiteheadRussell] p.
160 | Theorem *11.25 | 2nexaln 1928 |
[WhiteheadRussell] p.
161 | Theorem *11.3 | 19.21vv 39410 |
[WhiteheadRussell] p.
162 | Theorem *11.32 | 2alim 39411 |
[WhiteheadRussell] p.
162 | Theorem *11.33 | 2albi 39412 |
[WhiteheadRussell] p.
162 | Theorem *11.34 | 2exim 39413 |
[WhiteheadRussell] p.
162 | Theorem *11.36 | spsbce-2 39415 |
[WhiteheadRussell] p.
162 | Theorem *11.341 | 2exbi 39414 |
[WhiteheadRussell] p.
163 | Theorem *11.42 | 19.40-2 1989 |
[WhiteheadRussell] p.
163 | Theorem *11.43 | 19.36vv 39417 |
[WhiteheadRussell] p.
163 | Theorem *11.44 | 19.31vv 39418 |
[WhiteheadRussell] p.
163 | Theorem *11.421 | 19.33-2 39416 |
[WhiteheadRussell] p.
164 | Theorem *11.5 | 2nalexn 1926 |
[WhiteheadRussell] p.
164 | Theorem *11.46 | 19.37vv 39419 |
[WhiteheadRussell] p.
164 | Theorem *11.47 | 19.28vv 39420 |
[WhiteheadRussell] p.
164 | Theorem *11.51 | 2exnexn 1945 |
[WhiteheadRussell] p.
164 | Theorem *11.52 | pm11.52 39421 |
[WhiteheadRussell] p.
164 | Theorem *11.53 | pm11.53 2370 |
[WhiteheadRussell] p.
164 | Theorem *11.521 | 2exanali 39422 |
[WhiteheadRussell] p.
165 | Theorem *11.6 | pm11.6 39427 |
[WhiteheadRussell] p.
165 | Theorem *11.56 | aaanv 39423 |
[WhiteheadRussell] p.
165 | Theorem *11.57 | pm11.57 39424 |
[WhiteheadRussell] p.
165 | Theorem *11.58 | pm11.58 39425 |
[WhiteheadRussell] p.
165 | Theorem *11.59 | pm11.59 39426 |
[WhiteheadRussell] p.
166 | Theorem *11.7 | pm11.7 39431 |
[WhiteheadRussell] p.
166 | Theorem *11.61 | pm11.61 39428 |
[WhiteheadRussell] p.
166 | Theorem *11.62 | pm11.62 39429 |
[WhiteheadRussell] p.
166 | Theorem *11.63 | pm11.63 39430 |
[WhiteheadRussell] p.
166 | Theorem *11.71 | pm11.71 39432 |
[WhiteheadRussell] p.
175 | Definition *14.02 | df-eu 2640 |
[WhiteheadRussell] p.
178 | Theorem *13.13 | pm13.13a 39442 pm13.13b 39443 |
[WhiteheadRussell] p.
178 | Theorem *13.14 | pm13.14 39444 |
[WhiteheadRussell] p.
178 | Theorem *13.18 | pm13.18 3080 |
[WhiteheadRussell] p.
178 | Theorem *13.181 | pm13.181 3081 |
[WhiteheadRussell] p.
178 | Theorem *13.183 | pm13.183 3563 |
[WhiteheadRussell] p.
179 | Theorem *13.21 | 2sbc6g 39450 |
[WhiteheadRussell] p.
179 | Theorem *13.22 | 2sbc5g 39451 |
[WhiteheadRussell] p.
179 | Theorem *13.192 | pm13.192 39445 |
[WhiteheadRussell] p.
179 | Theorem *13.193 | 2pm13.193 39591 pm13.193 39446 |
[WhiteheadRussell] p.
179 | Theorem *13.194 | pm13.194 39447 |
[WhiteheadRussell] p.
179 | Theorem *13.195 | pm13.195 39448 |
[WhiteheadRussell] p.
179 | Theorem *13.196 | pm13.196a 39449 |
[WhiteheadRussell] p.
184 | Theorem *14.12 | pm14.12 39456 |
[WhiteheadRussell] p.
184 | Theorem *14.111 | iotasbc2 39455 |
[WhiteheadRussell] p.
184 | Definition *14.01 | iotasbc 39454 |
[WhiteheadRussell] p.
185 | Theorem *14.121 | sbeqalb 3715 |
[WhiteheadRussell] p.
185 | Theorem *14.122 | pm14.122a 39457 pm14.122b 39458 pm14.122c 39459 |
[WhiteheadRussell] p.
185 | Theorem *14.123 | pm14.123a 39460 pm14.123b 39461 pm14.123c 39462 |
[WhiteheadRussell] p.
189 | Theorem *14.2 | iotaequ 39464 |
[WhiteheadRussell] p.
189 | Theorem *14.18 | pm14.18 39463 |
[WhiteheadRussell] p.
189 | Theorem *14.202 | iotavalb 39465 |
[WhiteheadRussell] p.
190 | Theorem *14.22 | iota4 6108 |
[WhiteheadRussell] p.
190 | Theorem *14.205 | iotasbc5 39466 |
[WhiteheadRussell] p.
191 | Theorem *14.23 | iota4an 6109 |
[WhiteheadRussell] p.
191 | Theorem *14.24 | pm14.24 39467 |
[WhiteheadRussell] p.
192 | Theorem *14.25 | sbiota1 39469 |
[WhiteheadRussell] p.
192 | Theorem *14.26 | eupick 2716 eupickbi 2719 sbaniota 39470 |
[WhiteheadRussell] p.
192 | Theorem *14.242 | iotavalsb 39468 |
[WhiteheadRussell] p.
192 | Theorem *14.271 | eubi 2657 |
[WhiteheadRussell] p.
193 | Theorem *14.272 | iotasbcq 39472 |
[WhiteheadRussell] p.
235 | Definition *30.01 | conventions 27811 df-fv 6135 |
[WhiteheadRussell] p.
360 | Theorem *54.43 | pm54.43 9146 pm54.43lem 9145 |
[Young] p.
141 | Definition of operator ordering | leop2 29534 |
[Young] p.
142 | Example 12.2(i) | 0leop 29540 idleop 29541 |
[vandenDries] p. 42 | Lemma
61 | irrapx1 38231 |
[vandenDries] p. 43 | Theorem
62 | pellex 38238 pellexlem1 38232 |