Metamath Proof Explorer Home Metamath Proof Explorer
Bibliographic Cross-References
 
Mirrors  >  Home  >  MPE Home  >  Bibliographic Cross-References

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the Metamath Proof Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular set theory book, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

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

This page was last updated on 25-Oct-2021.
Copyright terms: Public domain