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 16042
[Adamek] p. 21Condition 3.1(b)df-cat 16042
[Adamek] p. 22Example 3.3(1)df-setc 16439
[Adamek] p. 24Example 3.3(4.c)0cat 16062
[Adamek] p. 25Definition 3.5df-oppc 16085
[Adamek] p. 28Remark 3.9oppciso 16154
[Adamek] p. 28Remark 3.12invf1o 16142  invisoinvl 16163
[Adamek] p. 28Example 3.13idinv 16162  idiso 16161
[Adamek] p. 28Corollary 3.11inveq 16147
[Adamek] p. 28Definition 3.8df-inv 16121  df-iso 16122  dfiso2 16145
[Adamek] p. 28Proposition 3.10sectcan 16128
[Adamek] p. 29Remark 3.16cicer 16179
[Adamek] p. 29Definition 3.15cic 16172  df-cic 16169
[Adamek] p. 29Definition 3.17df-func 16231
[Adamek] p. 29Proposition 3.14(1)invinv 16143
[Adamek] p. 29Proposition 3.14(2)invco 16144  isoco 16150
[Adamek] p. 30Remark 3.19df-func 16231
[Adamek] p. 30Example 3.20(1)idfucl 16254
[Adamek] p. 32Proposition 3.21funciso 16247
[Adamek] p. 33Proposition 3.23cofucl 16261
[Adamek] p. 34Remark 3.28(2)catciso 16470
[Adamek] p. 34Remark 3.28 (1)embedsetcestrc 16520
[Adamek] p. 34Definition 3.27(2)df-fth 16278
[Adamek] p. 34Definition 3.27(3)df-full 16277
[Adamek] p. 34Definition 3.27 (1)embedsetcestrc 16520
[Adamek] p. 35Corollary 3.32ffthiso 16302
[Adamek] p. 35Proposition 3.30(c)cofth 16308
[Adamek] p. 35Proposition 3.30(d)cofull 16307
[Adamek] p. 36Definition 3.33 (1)equivestrcsetc 16505
[Adamek] p. 36Definition 3.33 (2)equivestrcsetc 16505
[Adamek] p. 39Definition 3.41funcoppc 16248
[Adamek] p. 39Definition 3.44.df-catc 16458
[Adamek] p. 39Proposition 3.43(c)fthoppc 16296
[Adamek] p. 39Proposition 3.43(d)fulloppc 16295
[Adamek] p. 40Remark 3.48catccat 16467
[Adamek] p. 40Definition 3.47df-catc 16458
[Adamek] p. 48Example 4.3(1.a)0subcat 16211
[Adamek] p. 48Example 4.3(1.b)catsubcat 16212
[Adamek] p. 48Definition 4.1(2)fullsubc 16223
[Adamek] p. 48Definition 4.1(a)df-subc 16185
[Adamek] p. 49Remark 4.4(2)ressffth 16311
[Adamek] p. 83Definition 6.1df-nat 16316
[Adamek] p. 87Remark 6.14(a)fuccocl 16337
[Adamek] p. 87Remark 6.14(b)fucass 16341
[Adamek] p. 87Definition 6.15df-fuc 16317
[Adamek] p. 88Remark 6.16fuccat 16343
[Adamek] p. 101Definition 7.1df-inito 16354
[Adamek] p. 101Example 7.2 (6)irinitoringc 41953
[Adamek] p. 102Definition 7.4df-termo 16355
[Adamek] p. 102Proposition 7.3 (1)initoeu1w 16375
[Adamek] p. 102Proposition 7.3 (2)initoeu2 16379
[Adamek] p. 103Definition 7.7df-zeroo 16356
[Adamek] p. 103Example 7.9 (3)nzerooringczr 41956
[Adamek] p. 103Proposition 7.6termoeu1w 16382
[Adamek] p. 106Definition 7.19df-sect 16120
[Adamek] p. 478Item Rngdf-ringc 41889
[AhoHopUll] p. 2Section 1.1df-bigo 42232
[AhoHopUll] p. 12Section 1.3df-blen 42254
[AhoHopUll] p. 318Section 9.1df-concat 13013  df-pfx 40140  df-substr 13015  df-word 13011  lencl 13036  wrd0 13042
[AkhiezerGlazman] p. 39Linear operator normdf-nmo 22211  df-nmoo 26763
[AkhiezerGlazman] p. 64Theoremhmopidmch 28185  hmopidmchi 28183
[AkhiezerGlazman] p. 65Theorem 1pjcmul1i 28233  pjcmul2i 28234
[AkhiezerGlazman] p. 72Theoremcnvunop 27950  unoplin 27952
[AkhiezerGlazman] p. 72Equation 2unopadj 27951  unopadj2 27970
[AkhiezerGlazman] p. 73Theoremelunop2 28045  lnopunii 28044
[AkhiezerGlazman] p. 80Proposition 1adjlnop 28118
[Apostol] p. 18Theorem I.1addcan 9970  addcan2d 9990  addcan2i 9980  addcand 9989  addcani 9979
[Apostol] p. 18Theorem I.2negeu 10021
[Apostol] p. 18Theorem I.3negsub 10079  negsubd 10148  negsubi 10109
[Apostol] p. 18Theorem I.4negneg 10081  negnegd 10133  negnegi 10101
[Apostol] p. 18Theorem I.5subdi 10213  subdid 10235  subdii 10228  subdir 10214  subdird 10236  subdiri 10229
[Apostol] p. 18Theorem I.6mul01 9965  mul01d 9985  mul01i 9976  mul02 9964  mul02d 9984  mul02i 9975
[Apostol] p. 18Theorem I.7mulcan 10412  mulcan2d 10409  mulcand 10408  mulcani 10414
[Apostol] p. 18Theorem I.8receu 10420  xreceu 28757
[Apostol] p. 18Theorem I.9divrec 10449  divrecd 10552  divreci 10518  divreczi 10511
[Apostol] p. 18Theorem I.10recrec 10470  recreci 10505
[Apostol] p. 18Theorem I.11mul0or 10415  mul0ord 10425  mul0ori 10423
[Apostol] p. 18Theorem I.12mul2neg 10219  mul2negd 10234  mul2negi 10227  mulneg1 10216  mulneg1d 10232  mulneg1i 10225
[Apostol] p. 18Theorem I.13divadddiv 10488  divadddivd 10593  divadddivi 10535
[Apostol] p. 18Theorem I.14divmuldiv 10473  divmuldivd 10590  divmuldivi 10533  rdivmuldivd 28919
[Apostol] p. 18Theorem I.15divdivdiv 10474  divdivdivd 10596  divdivdivi 10536
[Apostol] p. 20Axiom 7rpaddcl 11595  rpaddcld 11628  rpmulcl 11596  rpmulcld 11629
[Apostol] p. 20Axiom 8rpneg 11604
[Apostol] p. 20Axiom 90nrp 11606
[Apostol] p. 20Theorem I.17lttri 9913
[Apostol] p. 20Theorem I.18ltadd1d 10368  ltadd1dd 10386  ltadd1i 10330
[Apostol] p. 20Theorem I.19ltmul1 10621  ltmul1a 10620  ltmul1i 10691  ltmul1ii 10701  ltmul2 10622  ltmul2d 11655  ltmul2dd 11669  ltmul2i 10694
[Apostol] p. 20Theorem I.20msqgt0 10296  msqgt0d 10343  msqgt0i 10313
[Apostol] p. 20Theorem I.210lt1 10298
[Apostol] p. 20Theorem I.23lt0neg1 10282  lt0neg1d 10345  ltneg 10276  ltnegd 10353  ltnegi 10320
[Apostol] p. 20Theorem I.25lt2add 10261  lt2addd 10398  lt2addi 10338
[Apostol] p. 20Definition of positive numbersdf-rp 11574
[Apostol] p. 21Exercise 4recgt0 10615  recgt0d 10707  recgt0i 10677  recgt0ii 10678
[Apostol] p. 22Definition of integersdf-z 11118
[Apostol] p. 22Definition of positive integersdfnn3 10788
[Apostol] p. 22Definition of rationalsdf-q 11530
[Apostol] p. 24Theorem I.26supeu 8118
[Apostol] p. 26Theorem I.28nnunb 11042
[Apostol] p. 26Theorem I.29arch 11043
[Apostol] p. 28Exercise 2btwnz 11218
[Apostol] p. 28Exercise 3nnrecl 11044
[Apostol] p. 28Exercise 4rebtwnz 11528
[Apostol] p. 28Exercise 5zbtwnre 11527
[Apostol] p. 28Exercise 6qbtwnre 11772
[Apostol] p. 28Exercise 10(a)zeneo 14768  zneo 11199  zneoALTV 40013
[Apostol] p. 29Theorem I.35msqsqrtd 13884  resqrtth 13701  sqrtth 13809  sqrtthi 13815  sqsqrtd 13883
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 10777
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwo 11492
[Apostol] p. 361Remarkcrreczi 12718
[Apostol] p. 363Remarkabsgt0i 13843
[Apostol] p. 363Exampleabssubd 13897  abssubi 13847
[ApostolNT] p. 7Remarkfmtno0 39885  fmtno1 39886  fmtno2 39895  fmtno3 39896  fmtno4 39897  fmtno5fac 39927  fmtnofz04prm 39922
[ApostolNT] p. 7Definitiondf-fmtno 39873
[ApostolNT] p. 8Definitiondf-ppi 24516
[ApostolNT] p. 14Definitiondf-dvds 14689
[ApostolNT] p. 14Theorem 1.1(a)iddvds 14700
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 14723
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 14719
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 14713
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 14715
[ApostolNT] p. 14Theorem 1.1(f)1dvds 14701
[ApostolNT] p. 14Theorem 1.1(g)dvds0 14702
[ApostolNT] p. 14Theorem 1.1(h)0dvds 14707
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 14738
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 14740
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 14742
[ApostolNT] p. 15Definitiondf-gcd 14926  dfgcd2 14975
[ApostolNT] p. 16Definitionisprm2 15107
[ApostolNT] p. 16Theorem 1.5coprmdvds 15078
[ApostolNT] p. 16Theorem 1.7prminf 15339
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 14944
[ApostolNT] p. 16Theorem 1.4(b)gcdass 14976
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 14978
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 14958
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 14950
[ApostolNT] p. 17Theorem 1.8coprm 15135
[ApostolNT] p. 17Theorem 1.9euclemma 15137
[ApostolNT] p. 17Theorem 1.101arith2 15352
[ApostolNT] p. 18Theorem 1.13prmrec 15346
[ApostolNT] p. 19Theorem 1.14divalg 14834
[ApostolNT] p. 20Theorem 1.15eucalg 15012
[ApostolNT] p. 24Definitiondf-mu 24517
[ApostolNT] p. 25Definitiondf-phi 15185
[ApostolNT] p. 25Theorem 2.1musum 24607
[ApostolNT] p. 26Theorem 2.2phisum 15209
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 15195
[ApostolNT] p. 28Theorem 2.5(c)phimul 15199
[ApostolNT] p. 32Definitiondf-vma 24514
[ApostolNT] p. 32Theorem 2.9muinv 24609
[ApostolNT] p. 32Theorem 2.10vmasum 24631
[ApostolNT] p. 38Remarkdf-sgm 24518
[ApostolNT] p. 38Definitiondf-sgm 24518
[ApostolNT] p. 75Definitiondf-chp 24515  df-cht 24513
[ApostolNT] p. 104Definitioncongr 15090
[ApostolNT] p. 106Remarkdvdsval3 14692
[ApostolNT] p. 106Definitionmoddvds 14696
[ApostolNT] p. 107Example 2mod2eq0even 14775
[ApostolNT] p. 107Example 3mod2eq1n2dvds 14776
[ApostolNT] p. 107Example 4zmod1congr 12416
[ApostolNT] p. 107Theorem 5.2(b)modmul12d 12453
[ApostolNT] p. 107Theorem 5.2(c)modexp 12728
[ApostolNT] p. 108Theorem 5.3modmulconst 14718
[ApostolNT] p. 109Theorem 5.4cncongr1 15093
[ApostolNT] p. 109Theorem 5.6gcdmodi 15498
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 15095
[ApostolNT] p. 113Theorem 5.17eulerth 15202
[ApostolNT] p. 113Theorem 5.18vfermltl 15226
[ApostolNT] p. 114Theorem 5.19fermltl 15203
[ApostolNT] p. 116Theorem 5.24wilthimp 24486
[ApostolNT] p. 179Definitiondf-lgs 24710  lgsprme0 24754
[ApostolNT] p. 180Example 11lgs 24755
[ApostolNT] p. 180Theorem 9.2lgsvalmod 24731
[ApostolNT] p. 180Theorem 9.3lgsdirprm 24746
[ApostolNT] p. 181Theorem 9.4m1lgs 24803
[ApostolNT] p. 181Theorem 9.52lgs 24822  2lgsoddprm 24831
[ApostolNT] p. 182Theorem 9.6gausslemma2d 24789
[ApostolNT] p. 185Theorem 9.8lgsquad 24798
[ApostolNT] p. 188Definitiondf-lgs 24710  lgs1 24756
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 24747
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 24749
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 24757
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 24758
[Baer] p. 40Property (b)mapdord 35820
[Baer] p. 40Property (c)mapd11 35821
[Baer] p. 40Property (e)mapdin 35844  mapdlsm 35846
[Baer] p. 40Property (f)mapd0 35847
[Baer] p. 40Definition of projectivitydf-mapd 35807  mapd1o 35830
[Baer] p. 41Property (g)mapdat 35849
[Baer] p. 44Part (1)mapdpg 35888
[Baer] p. 45Part (2)hdmap1eq 35984  mapdheq 35910  mapdheq2 35911  mapdheq2biN 35912
[Baer] p. 45Part (3)baerlem3 35895
[Baer] p. 46Part (4)mapdheq4 35914  mapdheq4lem 35913
[Baer] p. 46Part (5)baerlem5a 35896  baerlem5abmN 35900  baerlem5amN 35898  baerlem5b 35897  baerlem5bmN 35899
[Baer] p. 47Part (6)hdmap1l6 36004  hdmap1l6a 35992  hdmap1l6e 35997  hdmap1l6f 35998  hdmap1l6g 35999  hdmap1l6lem1 35990  hdmap1l6lem2 35991  hdmap1p6N 36005  mapdh6N 35929  mapdh6aN 35917  mapdh6eN 35922  mapdh6fN 35923  mapdh6gN 35924  mapdh6lem1N 35915  mapdh6lem2N 35916
[Baer] p. 48Part 9hdmapval 36013
[Baer] p. 48Part 10hdmap10 36025
[Baer] p. 48Part 11hdmapadd 36028
[Baer] p. 48Part (6)hdmap1l6h 36000  mapdh6hN 35925
[Baer] p. 48Part (7)mapdh75cN 35935  mapdh75d 35936  mapdh75e 35934  mapdh75fN 35937  mapdh7cN 35931  mapdh7dN 35932  mapdh7eN 35930  mapdh7fN 35933
[Baer] p. 48Part (8)mapdh8 35971  mapdh8a 35957  mapdh8aa 35958  mapdh8ab 35959  mapdh8ac 35960  mapdh8ad 35961  mapdh8b 35962  mapdh8c 35963  mapdh8d 35965  mapdh8d0N 35964  mapdh8e 35966  mapdh8fN 35967  mapdh8g 35968  mapdh8i 35969  mapdh8j 35970
[Baer] p. 48Part (9)mapdh9a 35972
[Baer] p. 48Equation 10mapdhvmap 35951
[Baer] p. 49Part 12hdmap11 36033  hdmapeq0 36029  hdmapf1oN 36050  hdmapneg 36031  hdmaprnN 36049  hdmaprnlem1N 36034  hdmaprnlem3N 36035  hdmaprnlem3uN 36036  hdmaprnlem4N 36038  hdmaprnlem6N 36039  hdmaprnlem7N 36040  hdmaprnlem8N 36041  hdmaprnlem9N 36042  hdmapsub 36032
[Baer] p. 49Part 14hdmap14lem1 36053  hdmap14lem10 36062  hdmap14lem1a 36051  hdmap14lem2N 36054  hdmap14lem2a 36052  hdmap14lem3 36055  hdmap14lem8 36060  hdmap14lem9 36061
[Baer] p. 50Part 14hdmap14lem11 36063  hdmap14lem12 36064  hdmap14lem13 36065  hdmap14lem14 36066  hdmap14lem15 36067  hgmapval 36072
[Baer] p. 50Part 15hgmapadd 36079  hgmapmul 36080  hgmaprnlem2N 36082  hgmapvs 36076
[Baer] p. 50Part 16hgmaprnN 36086
[Baer] p. 110Lemma 1hdmapip0com 36102
[Baer] p. 110Line 27hdmapinvlem1 36103
[Baer] p. 110Line 28hdmapinvlem2 36104
[Baer] p. 110Line 30hdmapinvlem3 36105
[Baer] p. 110Part 1.2hdmapglem5 36107  hgmapvv 36111
[Baer] p. 110Proposition 1hdmapinvlem4 36106
[Baer] p. 111Line 10hgmapvvlem1 36108
[Baer] p. 111Line 15hdmapg 36115  hdmapglem7 36114
[BellMachover] p. 36Lemma 10.3idALT 23
[BellMachover] p. 97Definition 10.1df-eu 2366
[BellMachover] p. 460Notationdf-mo 2367
[BellMachover] p. 460Definitionmo3 2399
[BellMachover] p. 461Axiom Extax-ext 2494
[BellMachover] p. 462Theorem 1.1bm1.1 2499
[BellMachover] p. 463Axiom Repaxrep5 4602
[BellMachover] p. 463Scheme Sepaxsep 4606
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4610
[BellMachover] p. 466Problemaxpow2 4670
[BellMachover] p. 466Axiom Powaxpow3 4671
[BellMachover] p. 466Axiom Unionaxun2 6724
[BellMachover] p. 468Definitiondf-ord 5533
[BellMachover] p. 469Theorem 2.2(i)ordirr 5548
[BellMachover] p. 469Theorem 2.2(iii)onelon 5555
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 5550
[BellMachover] p. 471Definition of Ndf-om 6833
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 6773
[BellMachover] p. 471Definition of Limdf-lim 5535
[BellMachover] p. 472Axiom Infzfinf2 8297
[BellMachover] p. 473Theorem 2.8limom 6847
[BellMachover] p. 477Equation 3.1df-r1 8385
[BellMachover] p. 478Definitionrankval2 8439
[BellMachover] p. 478Theorem 3.3(i)r1ord3 8403  r1ord3g 8400
[BellMachover] p. 480Axiom Regzfreg 8258
[BellMachover] p. 488Axiom ACac5 9057  dfac4 8703
[BellMachover] p. 490Definition of alephalephval3 8691
[BeltramettiCassinelli] p. 98Remarkatlatmstc 33499
[BeltramettiCassinelli] p. 107Remark 10.3.5atom1d 28385
[BeltramettiCassinelli] p. 166Theorem 14.8.4chirred 28427  chirredi 28426
[BeltramettiCassinelli1] p. 400Proposition P8(ii)atoml2i 28415
[Beran] p. 3Definition of joinsshjval3 27386
[Beran] p. 39Theorem 2.3(i)cmcm2 27648  cmcm2i 27625  cmcm2ii 27630  cmt2N 33430
[Beran] p. 40Theorem 2.3(iii)lecm 27649  lecmi 27634  lecmii 27635
[Beran] p. 45Theorem 3.4cmcmlem 27623
[Beran] p. 49Theorem 4.2cm2j 27652  cm2ji 27657  cm2mi 27658
[Beran] p. 95Definitiondf-sh 27237  issh2 27239
[Beran] p. 95Lemma 3.1(S5)his5 27116
[Beran] p. 95Lemma 3.1(S6)his6 27129
[Beran] p. 95Lemma 3.1(S7)his7 27120
[Beran] p. 95Lemma 3.2(S8)ho01i 27860
[Beran] p. 95Lemma 3.2(S9)hoeq1 27862
[Beran] p. 95Lemma 3.2(S10)ho02i 27861
[Beran] p. 95Lemma 3.2(S11)hoeq2 27863
[Beran] p. 95Postulate (S1)ax-his1 27112  his1i 27130
[Beran] p. 95Postulate (S2)ax-his2 27113
[Beran] p. 95Postulate (S3)ax-his3 27114
[Beran] p. 95Postulate (S4)ax-his4 27115
[Beran] p. 96Definition of normdf-hnorm 26998  dfhnorm2 27152  normval 27154
[Beran] p. 96Definition for Cauchy sequencehcau 27214
[Beran] p. 96Definition of Cauchy sequencedf-hcau 27003
[Beran] p. 96Definition of complete subspaceisch3 27271
[Beran] p. 96Definition of convergedf-hlim 27002  hlimi 27218
[Beran] p. 97Theorem 3.3(i)norm-i-i 27163  norm-i 27159
[Beran] p. 97Theorem 3.3(ii)norm-ii-i 27167  norm-ii 27168  normlem0 27139  normlem1 27140  normlem2 27141  normlem3 27142  normlem4 27143  normlem5 27144  normlem6 27145  normlem7 27146  normlem7tALT 27149
[Beran] p. 97Theorem 3.3(iii)norm-iii-i 27169  norm-iii 27170
[Beran] p. 98Remark 3.4bcs 27211  bcsiALT 27209  bcsiHIL 27210
[Beran] p. 98Remark 3.4(B)normlem9at 27151  normpar 27185  normpari 27184
[Beran] p. 98Remark 3.4(C)normpyc 27176  normpyth 27175  normpythi 27172
[Beran] p. 99Remarklnfn0 28079  lnfn0i 28074  lnop0 27998  lnop0i 28002
[Beran] p. 99Theorem 3.5(i)nmcexi 28058  nmcfnex 28085  nmcfnexi 28083  nmcopex 28061  nmcopexi 28059
[Beran] p. 99Theorem 3.5(ii)nmcfnlb 28086  nmcfnlbi 28084  nmcoplb 28062  nmcoplbi 28060
[Beran] p. 99Theorem 3.5(iii)lnfncon 28088  lnfnconi 28087  lnopcon 28067  lnopconi 28066
[Beran] p. 100Lemma 3.6normpar2i 27186
[Beran] p. 101Lemma 3.6norm3adifi 27183  norm3adifii 27178  norm3dif 27180  norm3difi 27177
[Beran] p. 102Theorem 3.7(i)chocunii 27333  pjhth 27425  pjhtheu 27426  pjpjhth 27457  pjpjhthi 27458  pjth 22894
[Beran] p. 102Theorem 3.7(ii)ococ 27438  ococi 27437
[Beran] p. 103Remark 3.8nlelchi 28093
[Beran] p. 104Theorem 3.9riesz3i 28094  riesz4 28096  riesz4i 28095
[Beran] p. 104Theorem 3.10cnlnadj 28111  cnlnadjeu 28110  cnlnadjeui 28109  cnlnadji 28108  cnlnadjlem1 28099  nmopadjlei 28120
[Beran] p. 106Theorem 3.11(i)adjeq0 28123
[Beran] p. 106Theorem 3.11(v)nmopadji 28122
[Beran] p. 106Theorem 3.11(ii)adjmul 28124
[Beran] p. 106Theorem 3.11(iv)adjadj 27968
[Beran] p. 106Theorem 3.11(vi)nmopcoadj2i 28134  nmopcoadji 28133
[Beran] p. 106Theorem 3.11(iii)adjadd 28125
[Beran] p. 106Theorem 3.11(vii)nmopcoadj0i 28135
[Beran] p. 106Theorem 3.11(viii)adjcoi 28132  pjadj2coi 28236  pjadjcoi 28193
[Beran] p. 107Definitiondf-ch 27251  isch2 27253
[Beran] p. 107Remark 3.12choccl 27338  isch3 27271  occl 27336  ocsh 27315  shoccl 27337  shocsh 27316
[Beran] p. 107Remark 3.12(B)ococin 27440
[Beran] p. 108Theorem 3.13chintcl 27364
[Beran] p. 109Property (i)pjadj2 28219  pjadj3 28220  pjadji 27717  pjadjii 27706
[Beran] p. 109Property (ii)pjidmco 28213  pjidmcoi 28209  pjidmi 27705
[Beran] p. 110Definition of projector orderingpjordi 28205
[Beran] p. 111Remarkho0val 27782  pjch1 27702
[Beran] p. 111Definitiondf-hfmul 27766  df-hfsum 27765  df-hodif 27764  df-homul 27763  df-hosum 27762
[Beran] p. 111Lemma 4.4(i)pjo 27703
[Beran] p. 111Lemma 4.4(ii)pjch 27726  pjchi 27464
[Beran] p. 111Lemma 4.4(iii)pjoc2 27471  pjoc2i 27470
[Beran] p. 112Theorem 4.5(i)->(ii)pjss2i 27712
[Beran] p. 112Theorem 4.5(i)->(iv)pjssmi 28197  pjssmii 27713
[Beran] p. 112Theorem 4.5(i)<->(ii)pjss2coi 28196
[Beran] p. 112Theorem 4.5(i)<->(iii)pjss1coi 28195
[Beran] p. 112Theorem 4.5(i)<->(vi)pjnormssi 28200
[Beran] p. 112Theorem 4.5(iv)->(v)pjssge0i 28198  pjssge0ii 27714
[Beran] p. 112Theorem 4.5(v)<->(vi)pjdifnormi 28199  pjdifnormii 27715
[Bobzien] p. 116Statement T3stoic3 1691
[Bobzien] p. 117Statement T2stoic2a 1689
[Bobzien] p. 117Statement T4stoic4a 1692
[Bobzien] p. 117Conclusion the contradictorystoic1a 1687
[Bogachev] p. 16Definition 1.5df-oms 29479
[Bogachev] p. 17Lemma 1.5.4omssubadd 29492
[Bogachev] p. 17Example 1.5.2omsmon 29490
[Bogachev] p. 41Definition 1.11.2df-carsg 29498
[Bogachev] p. 42Theorem 1.11.4carsgsiga 29518
[Bogachev] p. 116Definition 2.3.1df-itgm 29550  df-sitm 29528
[Bogachev] p. 118Chapter 2.4.4df-itgm 29550
[Bogachev] p. 118Definition 2.4.1df-sitg 29527
[Bollobas] p. 1Section I.1df-edg 25604  df-edga 40444  isuhgrop 40387  isusgrop 40484  uhgraop 25572
[Bollobas] p. 2Section I.1df-subgr 40584  uhgrspan1 40619  uhgrspansubgr 40607
[Bollobas] p. 3Section I.1cusgrsize 40762  df-cusgr 40650  df-nbgr 40646  fusgrmaxsize 40772
[Bollobas] p. 4Definitiondf-1wlks 40892  df-wlk 25775  df-wlks 40893
[Bollobas] p. 5Notationdf-pth 25777  df-pths 41015
[Bollobas] p. 5Definitiondf-crct 25779  df-crcts 41084  df-cycl 25780  df-cycls 41085  df-trail 25776  df-trls 40993  df-wlkon 25781  df-wlkson 40894
[Bollobas] p. 7Section I.1df-ushgr 40373
[BourbakiAlg1] p. 1Definition 1df-clintop 41718  df-cllaw 41704  df-mgm 16955  df-mgm2 41737
[BourbakiAlg1] p. 4Definition 5df-assintop 41719  df-asslaw 41706  df-sgrp 16997  df-sgrp2 41739
[BourbakiAlg1] p. 7Definition 8df-cmgm2 41738  df-comlaw 41705
[BourbakiAlg1] p. 12Definition 2df-mnd 17008
[BourbakiAlg1] p. 92Definition 1df-ring 18277
[BourbakiAlg1] p. 93Section I.8.1df-rng0 41757
[BourbakiEns] p. Proposition 8fcof1 6318  fcofo 6319
[BourbakiTop1] p. Remarkxnegmnf 11783  xnegpnf 11782
[BourbakiTop1] p. Remark rexneg 11784
[BourbakiTop1] p. Theoremneiss 20624
[BourbakiTop1] p. Remark 3ust0 21734  ustfilxp 21727
[BourbakiTop1] p. Axiom GT'tgpsubcn 21605
[BourbakiTop1] p. Example 1cstucnd 21799  iducn 21798  snfil 21379
[BourbakiTop1] p. Example 2neifil 21395
[BourbakiTop1] p. Theorem 1cnextcn 21582
[BourbakiTop1] p. Theorem 2ucnextcn 21819
[BourbakiTop1] p. Theorem 3df-hcmp 29128
[BourbakiTop1] p. Definitionistgp 21592
[BourbakiTop1] p. Paragraph 3infil 21378
[BourbakiTop1] p. Propositioncnpco 20782  ishmeo 21273  neips 20628
[BourbakiTop1] p. Definition 1df-ucn 21791  df-ust 21715  filintn0 21376  ucnprima 21797
[BourbakiTop1] p. Definition 2df-cfilu 21802
[BourbakiTop1] p. Definition 3df-cusp 21813  df-usp 21772  df-utop 21746  trust 21744
[BourbakiTop1] p. Definition 6df-pcmp 29048
[BourbakiTop1] p. Condition F_Iustssel 21720
[BourbakiTop1] p. Condition U_Iustdiag 21723
[BourbakiTop1] p. Property V_ivneiptopreu 20648
[BourbakiTop1] p. Proposition 1ucncn 21800  ustund 21736  ustuqtop 21761
[BourbakiTop1] p. Proposition 2neiptopreu 20648  utop2nei 21765  utop3cls 21766
[BourbakiTop1] p. Proposition 3fmucnd 21807  uspreg 21789  utopreg 21767
[BourbakiTop1] p. Proposition 4imasncld 21205  imasncls 21206  imasnopn 21204
[BourbakiTop1] p. Proposition 9cnpflf2 21515
[BourbakiTop1] p. Theorem 1 (d)iscncl 20784
[BourbakiTop1] p. Condition F_IIustincl 21722
[BourbakiTop1] p. Condition U_IIustinvel 21724
[BourbakiTop1] p. Proposition 11cnextucn 21818
[BourbakiTop1] p. Proposition Vissnei2 20631
[BourbakiTop1] p. Condition F_IIbustbasel 21721
[BourbakiTop1] p. Condition U_IIIustexhalf 21725
[BourbakiTop1] p. Definition C'''df-cmp 20901
[BourbakiTop1] p. Proposition Viiinnei 20640
[BourbakiTop1] p. Proposition Vivneissex 20642
[BourbakiTop1] p. Proposition Viiielnei 20626  ssnei 20625
[BourbakiTop1] p. Remark below def. 1filn0 21377
[BourbakiTop1] p. Axioms FI, FIIa, FIIb, FIII)df-fil 21361
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 20422
[BourbakiTop2] p. 195Definition 1df-ldlf 29045
[BrosowskiDeutsh] p. 89Proof follows stoweidlem62 38845
[BrosowskiDeutsh] p. 89Lemmas are written following stowei 38847  stoweid 38846
[BrosowskiDeutsh] p. 90Lemma 1stoweidlem1 38784  stoweidlem10 38793  stoweidlem14 38797  stoweidlem15 38798  stoweidlem35 38818  stoweidlem36 38819  stoweidlem37 38820  stoweidlem38 38821  stoweidlem40 38823  stoweidlem41 38824  stoweidlem43 38826  stoweidlem44 38827  stoweidlem46 38829  stoweidlem5 38788  stoweidlem50 38833  stoweidlem52 38835  stoweidlem53 38836  stoweidlem55 38838  stoweidlem56 38839
[BrosowskiDeutsh] p. 90Lemma 1 stoweidlem23 38806  stoweidlem24 38807  stoweidlem27 38810  stoweidlem28 38811  stoweidlem30 38813
[BrosowskiDeutsh] p. 91Proofstoweidlem34 38817  stoweidlem59 38842  stoweidlem60 38843
[BrosowskiDeutsh] p. 91Lemma 1stoweidlem45 38828  stoweidlem49 38832  stoweidlem7 38790
[BrosowskiDeutsh] p. 91Lemma 2stoweidlem31 38814  stoweidlem39 38822  stoweidlem42 38825  stoweidlem48 38831  stoweidlem51 38834  stoweidlem54 38837  stoweidlem57 38840  stoweidlem58 38841
[BrosowskiDeutsh] p. 91Lemma 1 stoweidlem25 38808
[BrosowskiDeutsh] p. 91Lemma proves that the function ` ` (as definedstoweidlem17 38800
[BrosowskiDeutsh] p. 92Proofstoweidlem11 38794  stoweidlem13 38796  stoweidlem26 38809  stoweidlem61 38844
[BrosowskiDeutsh] p. 92Lemma 2stoweidlem18 38801
[Bruck] p. 1Section I.1df-clintop 41718  df-mgm 16955  df-mgm2 41737
[Bruck] p. 23Section II.1df-sgrp 16997  df-sgrp2 41739
[Bruck] p. 28Theorem 3.2dfgrp3 17227
[ChoquetDD] p. 2Definition of mappingdf-mpt 4543
[Church] p. 129Section II.24df-ifp 1006  dfifp2 1007
[Clemente] p. 10Definition ITnatded 26391
[Clemente] p. 10Definition I` `m,nnatded 26391
[Clemente] p. 11Definition E=>m,nnatded 26391
[Clemente] p. 11Definition I=>m,nnatded 26391
[Clemente] p. 11Definition E` `(1)natded 26391
[Clemente] p. 11Definition E` `(2)natded 26391
[Clemente] p. 12Definition E` `m,n,pnatded 26391
[Clemente] p. 12Definition I` `n(1)natded 26391
[Clemente] p. 12Definition I` `n(2)natded 26391
[Clemente] p. 13Definition I` `m,n,pnatded 26391
[Clemente] p. 14Proof 5.11natded 26391
[Clemente] p. 14Definition E` `nnatded 26391
[Clemente] p. 15Theorem 5.2ex-natded5.2-2 26393  ex-natded5.2 26392
[Clemente] p. 16Theorem 5.3ex-natded5.3-2 26396  ex-natded5.3 26395
[Clemente] p. 18Theorem 5.5ex-natded5.5 26398
[Clemente] p. 19Theorem 5.7ex-natded5.7-2 26400  ex-natded5.7 26399
[Clemente] p. 20Theorem 5.8ex-natded5.8-2 26402  ex-natded5.8 26401
[Clemente] p. 20Theorem 5.13ex-natded5.13-2 26404  ex-natded5.13 26403
[Clemente] p. 32Definition I` `nnatded 26391
[Clemente] p. 32Definition E` `m,n,p,anatded 26391
[Clemente] p. 32Definition E` `n,tnatded 26391
[Clemente] p. 32Definition I` `n,tnatded 26391
[Clemente] p. 43Theorem 9.20ex-natded9.20 26405
[Clemente] p. 45Theorem 9.20ex-natded9.20-2 26406
[Clemente] p. 45Theorem 9.26ex-natded9.26-2 26408  ex-natded9.26 26407
[Cohen] p. 301Remarkrelogoprlem 24029
[Cohen] p. 301Property 2relogmul 24030  relogmuld 24063
[Cohen] p. 301Property 3relogdiv 24031  relogdivd 24064
[Cohen] p. 301Property 4relogexp 24034
[Cohen] p. 301Property 1alog1 24024
[Cohen] p. 301Property 1bloge 24025
[Cohen4] p. 348Observationrelogbcxpb 24213
[Cohen4] p. 349Propertyrelogbf 24217
[Cohen4] p. 352Definitionelogb 24196
[Cohen4] p. 361Property 2relogbmul 24203
[Cohen4] p. 361Property 3logbrec 24208  relogbdiv 24205
[Cohen4] p. 361Property 4relogbreexp 24201
[Cohen4] p. 361Property 6relogbexp 24206
[Cohen4] p. 361Property 1(a)logbid1 24194
[Cohen4] p. 361Property 1(b)logb1 24195
[Cohen4] p. 367Propertylogbchbase 24197
[Cohen4] p. 377Property 2logblt 24210
[Cohn] p. 4Proposition 1.1.5sxbrsigalem1 29471  sxbrsigalem4 29473
[Cohn] p. 81Section II.5acsdomd 16894  acsinfd 16893  acsinfdimd 16895  acsmap2d 16892  acsmapd 16891
[Cohn] p. 143Example 5.1.1sxbrsiga 29476
[Connell] p. 57Definitiondf-scmat 20017  df-scmatalt 42074
[CormenLeisersonRivest] p. 33Equation 2.4fldiv2 12389
[Crawley] p. 1Definition of posetdf-poset 16659
[Crawley] p. 107Theorem 13.2hlsupr 33565
[Crawley] p. 110Theorem 13.3arglem1N 34370  dalaw 34065
[Crawley] p. 111Theorem 13.4hlathil 36146
[Crawley] p. 111Definition of set Wdf-watsN 34169
[Crawley] p. 111Definition of dilationdf-dilN 34285  df-ldil 34283  isldil 34289
[Crawley] p. 111Definition of translationdf-ltrn 34284  df-trnN 34286  isltrn 34298  ltrnu 34300
[Crawley] p. 112Lemma Acdlema1N 33970  cdlema2N 33971  exatleN 33583
[Crawley] p. 112Lemma B1cvrat 33655  cdlemb 33973  cdlemb2 34220  cdlemb3 34787  idltrn 34329  l1cvat 33235  lhpat 34222  lhpat2 34224  lshpat 33236  ltrnel 34318  ltrnmw 34330
[Crawley] p. 112Lemma Ccdlemc1 34371  cdlemc2 34372  ltrnnidn 34354  trlat 34349  trljat1 34346  trljat2 34347  trljat3 34348  trlne 34365  trlnidat 34353  trlnle 34366
[Crawley] p. 112Definition of automorphismdf-pautN 34170
[Crawley] p. 113Lemma Ccdlemc 34377  cdlemc3 34373  cdlemc4 34374
[Crawley] p. 113Lemma Dcdlemd 34387  cdlemd1 34378  cdlemd2 34379  cdlemd3 34380  cdlemd4 34381  cdlemd5 34382  cdlemd6 34383  cdlemd7 34384  cdlemd8 34385  cdlemd9 34386  cdleme31sde 34566  cdleme31se 34563  cdleme31se2 34564  cdleme31snd 34567  cdleme32a 34622  cdleme32b 34623  cdleme32c 34624  cdleme32d 34625  cdleme32e 34626  cdleme32f 34627  cdleme32fva 34618  cdleme32fva1 34619  cdleme32fvcl 34621  cdleme32le 34628  cdleme48fv 34680  cdleme4gfv 34688  cdleme50eq 34722  cdleme50f 34723  cdleme50f1 34724  cdleme50f1o 34727  cdleme50laut 34728  cdleme50ldil 34729  cdleme50lebi 34721  cdleme50rn 34726  cdleme50rnlem 34725  cdlemeg49le 34692  cdlemeg49lebilem 34720
[Crawley] p. 113Lemma Ecdleme 34741  cdleme00a 34389  cdleme01N 34401  cdleme02N 34402  cdleme0a 34391  cdleme0aa 34390  cdleme0b 34392  cdleme0c 34393  cdleme0cp 34394  cdleme0cq 34395  cdleme0dN 34396  cdleme0e 34397  cdleme0ex1N 34403  cdleme0ex2N 34404  cdleme0fN 34398  cdleme0gN 34399  cdleme0moN 34405  cdleme1 34407  cdleme10 34434  cdleme10tN 34438  cdleme11 34450  cdleme11a 34440  cdleme11c 34441  cdleme11dN 34442  cdleme11e 34443  cdleme11fN 34444  cdleme11g 34445  cdleme11h 34446  cdleme11j 34447  cdleme11k 34448  cdleme11l 34449  cdleme12 34451  cdleme13 34452  cdleme14 34453  cdleme15 34458  cdleme15a 34454  cdleme15b 34455  cdleme15c 34456  cdleme15d 34457  cdleme16 34465  cdleme16aN 34439  cdleme16b 34459  cdleme16c 34460  cdleme16d 34461  cdleme16e 34462  cdleme16f 34463  cdleme16g 34464  cdleme19a 34484  cdleme19b 34485  cdleme19c 34486  cdleme19d 34487  cdleme19e 34488  cdleme19f 34489  cdleme1b 34406  cdleme2 34408  cdleme20aN 34490  cdleme20bN 34491  cdleme20c 34492  cdleme20d 34493  cdleme20e 34494  cdleme20f 34495  cdleme20g 34496  cdleme20h 34497  cdleme20i 34498  cdleme20j 34499  cdleme20k 34500  cdleme20l 34503  cdleme20l1 34501  cdleme20l2 34502  cdleme20m 34504  cdleme20y 34482  cdleme20zN 34481  cdleme21 34518  cdleme21d 34511  cdleme21e 34512  cdleme22a 34521  cdleme22aa 34520  cdleme22b 34522  cdleme22cN 34523  cdleme22d 34524  cdleme22e 34525  cdleme22eALTN 34526  cdleme22f 34527  cdleme22f2 34528  cdleme22g 34529  cdleme23a 34530  cdleme23b 34531  cdleme23c 34532  cdleme26e 34540  cdleme26eALTN 34542  cdleme26ee 34541  cdleme26f 34544  cdleme26f2 34546  cdleme26f2ALTN 34545  cdleme26fALTN 34543  cdleme27N 34550  cdleme27a 34548  cdleme27cl 34547  cdleme28c 34553  cdleme3 34417  cdleme30a 34559  cdleme31fv 34571  cdleme31fv1 34572  cdleme31fv1s 34573  cdleme31fv2 34574  cdleme31id 34575  cdleme31sc 34565  cdleme31sdnN 34568  cdleme31sn 34561  cdleme31sn1 34562  cdleme31sn1c 34569  cdleme31sn2 34570  cdleme31so 34560  cdleme35a 34629  cdleme35b 34631  cdleme35c 34632  cdleme35d 34633  cdleme35e 34634  cdleme35f 34635  cdleme35fnpq 34630  cdleme35g 34636  cdleme35h 34637  cdleme35h2 34638  cdleme35sn2aw 34639  cdleme35sn3a 34640  cdleme36a 34641  cdleme36m 34642  cdleme37m 34643  cdleme38m 34644  cdleme38n 34645  cdleme39a 34646  cdleme39n 34647  cdleme3b 34409  cdleme3c 34410  cdleme3d 34411  cdleme3e 34412  cdleme3fN 34413  cdleme3fa 34416  cdleme3g 34414  cdleme3h 34415  cdleme4 34418  cdleme40m 34648  cdleme40n 34649  cdleme40v 34650  cdleme40w 34651  cdleme41fva11 34658  cdleme41sn3aw 34655  cdleme41sn4aw 34656  cdleme41snaw 34657  cdleme42a 34652  cdleme42b 34659  cdleme42c 34653  cdleme42d 34654  cdleme42e 34660  cdleme42f 34661  cdleme42g 34662  cdleme42h 34663  cdleme42i 34664  cdleme42k 34665  cdleme42ke 34666  cdleme42keg 34667  cdleme42mN 34668  cdleme42mgN 34669  cdleme43aN 34670  cdleme43bN 34671  cdleme43cN 34672  cdleme43dN 34673  cdleme5 34420  cdleme50ex 34740  cdleme50ltrn 34738  cdleme51finvN 34737  cdleme51finvfvN 34736  cdleme51finvtrN 34739  cdleme6 34421  cdleme7 34429  cdleme7a 34423  cdleme7aa 34422  cdleme7b 34424  cdleme7c 34425  cdleme7d 34426  cdleme7e 34427  cdleme7ga 34428  cdleme8 34430  cdleme8tN 34435  cdleme9 34433  cdleme9a 34431  cdleme9b 34432  cdleme9tN 34437  cdleme9taN 34436  cdlemeda 34478  cdlemedb 34477  cdlemednpq 34479  cdlemednuN 34480  cdlemefr27cl 34584  cdlemefr32fva1 34591  cdlemefr32fvaN 34590  cdlemefrs32fva 34581  cdlemefrs32fva1 34582  cdlemefs27cl 34594  cdlemefs32fva1 34604  cdlemefs32fvaN 34603  cdlemesner 34476  cdlemeulpq 34400
[Crawley] p. 114Lemma E4atex 34255  4atexlem7 34254  cdleme0nex 34470  cdleme17a 34466  cdleme17c 34468  cdleme17d 34679  cdleme17d1 34469  cdleme17d2 34676  cdleme18a 34471  cdleme18b 34472  cdleme18c 34473  cdleme18d 34475  cdleme4a 34419
[Crawley] p. 115Lemma Ecdleme21a 34506  cdleme21at 34509  cdleme21b 34507  cdleme21c 34508  cdleme21ct 34510  cdleme21f 34513  cdleme21g 34514  cdleme21h 34515  cdleme21i 34516  cdleme22gb 34474
[Crawley] p. 116Lemma Fcdlemf 34744  cdlemf1 34742  cdlemf2 34743
[Crawley] p. 116Lemma Gcdlemftr1 34748  cdlemg16 34838  cdlemg28 34885  cdlemg28a 34874  cdlemg28b 34884  cdlemg3a 34778  cdlemg42 34910  cdlemg43 34911  cdlemg44 34914  cdlemg44a 34912  cdlemg46 34916  cdlemg47 34917  cdlemg9 34815  ltrnco 34900  ltrncom 34919  tgrpabl 34932  trlco 34908
[Crawley] p. 116Definition of Gdf-tgrp 34924
[Crawley] p. 117Lemma Gcdlemg17 34858  cdlemg17b 34843
[Crawley] p. 117Definition of Edf-edring-rN 34937  df-edring 34938
[Crawley] p. 117Definition of trace-preserving endomorphismistendo 34941
[Crawley] p. 118Remarktendopltp 34961
[Crawley] p. 118Lemma Hcdlemh 34998  cdlemh1 34996  cdlemh2 34997
[Crawley] p. 118Lemma Icdlemi 35001  cdlemi1 34999  cdlemi2 35000
[Crawley] p. 118Lemma Jcdlemj1 35002  cdlemj2 35003  cdlemj3 35004  tendocan 35005
[Crawley] p. 118Lemma Kcdlemk 35155  cdlemk1 35012  cdlemk10 35024  cdlemk11 35030  cdlemk11t 35127  cdlemk11ta 35110  cdlemk11tb 35112  cdlemk11tc 35126  cdlemk11u-2N 35070  cdlemk11u 35052  cdlemk12 35031  cdlemk12u-2N 35071  cdlemk12u 35053  cdlemk13-2N 35057  cdlemk13 35033  cdlemk14-2N 35059  cdlemk14 35035  cdlemk15-2N 35060  cdlemk15 35036  cdlemk16-2N 35061  cdlemk16 35038  cdlemk16a 35037  cdlemk17-2N 35062  cdlemk17 35039  cdlemk18-2N 35067  cdlemk18-3N 35081  cdlemk18 35049  cdlemk19-2N 35068  cdlemk19 35050  cdlemk19u 35151  cdlemk1u 35040  cdlemk2 35013  cdlemk20-2N 35073  cdlemk20 35055  cdlemk21-2N 35072  cdlemk21N 35054  cdlemk22-3 35082  cdlemk22 35074  cdlemk23-3 35083  cdlemk24-3 35084  cdlemk25-3 35085  cdlemk26-3 35087  cdlemk26b-3 35086  cdlemk27-3 35088  cdlemk28-3 35089  cdlemk29-3 35092  cdlemk3 35014  cdlemk30 35075  cdlemk31 35077  cdlemk32 35078  cdlemk33N 35090  cdlemk34 35091  cdlemk35 35093  cdlemk36 35094  cdlemk37 35095  cdlemk38 35096  cdlemk39 35097  cdlemk39u 35149  cdlemk4 35015  cdlemk41 35101  cdlemk42 35122  cdlemk42yN 35125  cdlemk43N 35144  cdlemk45 35128  cdlemk46 35129  cdlemk47 35130  cdlemk48 35131  cdlemk49 35132  cdlemk5 35017  cdlemk50 35133  cdlemk51 35134  cdlemk52 35135  cdlemk53 35138  cdlemk54 35139  cdlemk55 35142  cdlemk55u 35147  cdlemk56 35152  cdlemk5a 35016  cdlemk5auN 35041  cdlemk5u 35042  cdlemk6 35018  cdlemk6u 35043  cdlemk7 35029  cdlemk7u-2N 35069  cdlemk7u 35051  cdlemk8 35019  cdlemk9 35020  cdlemk9bN 35021  cdlemki 35022  cdlemkid 35117  cdlemkj-2N 35063  cdlemkj 35044  cdlemksat 35027  cdlemksel 35026  cdlemksv 35025  cdlemksv2 35028  cdlemkuat 35047  cdlemkuel-2N 35065  cdlemkuel-3 35079  cdlemkuel 35046  cdlemkuv-2N 35064  cdlemkuv2-2 35066  cdlemkuv2-3N 35080  cdlemkuv2 35048  cdlemkuvN 35045  cdlemkvcl 35023  cdlemky 35107  cdlemkyyN 35143  tendoex 35156
[Crawley] p. 120Remarkdva1dim 35166
[Crawley] p. 120Lemma Lcdleml1N 35157  cdleml2N 35158  cdleml3N 35159  cdleml4N 35160  cdleml5N 35161  cdleml6 35162  cdleml7 35163  cdleml8 35164  cdleml9 35165  dia1dim 35243
[Crawley] p. 120Lemma Mdia11N 35230  diaf11N 35231  dialss 35228  diaord 35229  dibf11N 35343  djajN 35319
[Crawley] p. 120Definition of isomorphism mapdiaval 35214
[Crawley] p. 121Lemma Mcdlemm10N 35300  dia2dimlem1 35246  dia2dimlem2 35247  dia2dimlem3 35248  dia2dimlem4 35249  dia2dimlem5 35250  diaf1oN 35312  diarnN 35311  dvheveccl 35294  dvhopN 35298
[Crawley] p. 121Lemma Ncdlemn 35394  cdlemn10 35388  cdlemn11 35393  cdlemn11a 35389  cdlemn11b 35390  cdlemn11c 35391  cdlemn11pre 35392  cdlemn2 35377  cdlemn2a 35378  cdlemn3 35379  cdlemn4 35380  cdlemn4a 35381  cdlemn5 35383  cdlemn5pre 35382  cdlemn6 35384  cdlemn7 35385  cdlemn8 35386  cdlemn9 35387  diclspsn 35376
[Crawley] p. 121Definition of phi(q)df-dic 35355
[Crawley] p. 122Lemma Ndih11 35447  dihf11 35449  dihjust 35399  dihjustlem 35398  dihord 35446  dihord1 35400  dihord10 35405  dihord11b 35404  dihord11c 35406  dihord2 35409  dihord2a 35401  dihord2b 35402  dihord2cN 35403  dihord2pre 35407  dihord2pre2 35408  dihordlem6 35395  dihordlem7 35396  dihordlem7b 35397
[Crawley] p. 122Definition of isomorphism mapdihffval 35412  dihfval 35413  dihval 35414
[Diestel] p. 3Section 1.1df-cusgr 40650  df-nbgr 40646
[Diestel] p. 4Section 1.1df-subgr 40584  uhgrspan1 40619  uhgrspansubgr 40607
[Diestel] p. 27Section 1.10df-ushgr 40373
[Eisenberg] p. 67Definition 5.3df-dif 3447
[Eisenberg] p. 82Definition 6.3dfom3 8302
[Eisenberg] p. 125Definition 8.21df-map 7621
[Eisenberg] p. 216Example 13.2(4)omenps 8310
[Eisenberg] p. 310Theorem 19.8cardprc 8564
[Eisenberg] p. 310Corollary 19.7(2)cardsdom 9131
[Enderton] p. 18Axiom of Empty Setaxnul 4614
[Enderton] p. 19Definitiondf-tp 4033
[Enderton] p. 26Exercise 5unissb 4303
[Enderton] p. 26Exercise 10pwel 4745
[Enderton] p. 28Exercise 7(b)pwun 4840
[Enderton] p. 30Theorem "Distributive laws"iinin1 4425  iinin2 4424  iinun2 4420  iunin1 4419  iunin1f 28546  iunin2 4418  uniin1 28539  uniin2 28540
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4423  iundif2 4421
[Enderton] p. 32Exercise 20unineq 3739
[Enderton] p. 33Exercise 23iinuni 4443
[Enderton] p. 33Exercise 25iununi 4444
[Enderton] p. 33Exercise 24(a)iinpw 4448
[Enderton] p. 33Exercise 24(b)iunpw 6745  iunpwss 4449
[Enderton] p. 36Definitionopthwiener 4796
[Enderton] p. 38Exercise 6(a)unipw 4743
[Enderton] p. 38Exercise 6(b)pwuni 4724
[Enderton] p. 41Lemma 3Dopeluu 4764  rnex 6867  rnexg 6865
[Enderton] p. 41Exercise 8dmuni 5147  rnuni 5353
[Enderton] p. 42Definition of a functiondffun7 5715  dffun8 5716
[Enderton] p. 43Definition of function valuefunfv2 6059
[Enderton] p. 43Definition of single-rootedfuncnv 5757
[Enderton] p. 44Definition (d)dfima2 5277  dfima3 5278
[Enderton] p. 47Theorem 3Hfvco2 6066
[Enderton] p. 49Axiom of Choice (first form)ac7 9053  ac7g 9054  df-ac 8697  dfac2 8711  dfac2a 8710  dfac3 8702  dfac7 8712
[Enderton] p. 50Theorem 3K(a)imauni 6284
[Enderton] p. 52Definitiondf-map 7621
[Enderton] p. 53Exercise 21coass 5461
[Enderton] p. 53Exercise 27dmco 5450
[Enderton] p. 53Exercise 14(a)funin 5764
[Enderton] p. 53Exercise 22(a)imass2 5311
[Enderton] p. 54Remarkixpf 7691  ixpssmap 7703
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 7670
[Enderton] p. 55Axiom of Choice (second form)ac9 9063  ac9s 9073
[Enderton] p. 56Theorem 3Merref 7524
[Enderton] p. 57Lemma 3Nerthi 7555
[Enderton] p. 57Definitiondf-ec 7506
[Enderton] p. 58Definitiondf-qs 7510
[Enderton] p. 61Exercise 35df-ec 7506
[Enderton] p. 65Exercise 56(a)dmun 5144
[Enderton] p. 68Definition of successordf-suc 5536
[Enderton] p. 71Definitiondf-tr 4579  dftr4 4583
[Enderton] p. 72Theorem 4Eunisuc 5606
[Enderton] p. 73Exercise 6unisuc 5606
[Enderton] p. 73Exercise 5(a)truni 4593
[Enderton] p. 73Exercise 5(b)trint 4594  trintALT 38021
[Enderton] p. 79Theorem 4I(A1)nna0 7446
[Enderton] p. 79Theorem 4I(A2)nnasuc 7448  onasuc 7370
[Enderton] p. 79Definition of operation valuedf-ov 6428
[Enderton] p. 80Theorem 4J(A1)nnm0 7447
[Enderton] p. 80Theorem 4J(A2)nnmsuc 7449  onmsuc 7371
[Enderton] p. 81Theorem 4K(1)nnaass 7464
[Enderton] p. 81Theorem 4K(2)nna0r 7451  nnacom 7459
[Enderton] p. 81Theorem 4K(3)nndi 7465
[Enderton] p. 81Theorem 4K(4)nnmass 7466
[Enderton] p. 81Theorem 4K(5)nnmcom 7468
[Enderton] p. 82Exercise 16nnm0r 7452  nnmsucr 7467
[Enderton] p. 88Exercise 23nnaordex 7480
[Enderton] p. 129Definitiondf-en 7717
[Enderton] p. 132Theorem 6B(b)canth 6384
[Enderton] p. 133Exercise 1xpomen 8596
[Enderton] p. 133Exercise 2qnnen 14648
[Enderton] p. 134Theorem (Pigeonhole Principle)php 7904
[Enderton] p. 135Corollary 6Cphp3 7906
[Enderton] p. 136Corollary 6Enneneq 7903
[Enderton] p. 136Corollary 6D(a)pssinf 7930
[Enderton] p. 136Corollary 6D(b)ominf 7932
[Enderton] p. 137Lemma 6Fpssnn 7938
[Enderton] p. 138Corollary 6Gssfi 7940
[Enderton] p. 139Theorem 6H(c)mapen 7884
[Enderton] p. 142Theorem 6I(3)xpcdaen 8763
[Enderton] p. 142Theorem 6I(4)mapcdaen 8764
[Enderton] p. 143Theorem 6Jcda0en 8759  cda1en 8755
[Enderton] p. 144Exercise 13iunfi 8012  unifi 8013  unifi2 8014
[Enderton] p. 144Corollary 6Kundif2 3899  unfi 7987  unfi2 7989
[Enderton] p. 145Figure 38ffoss 6894
[Enderton] p. 145Definitiondf-dom 7718
[Enderton] p. 146Example 1domen 7729  domeng 7730
[Enderton] p. 146Example 3nndomo 7914  nnsdom 8309  nnsdomg 7979
[Enderton] p. 149Theorem 6L(a)cdadom2 8767
[Enderton] p. 149Theorem 6L(c)mapdom1 7885  xpdom1 7819  xpdom1g 7817  xpdom2g 7816
[Enderton] p. 149Theorem 6L(d)mapdom2 7891
[Enderton] p. 151Theorem 6Mzorn 9087  zorng 9084
[Enderton] p. 151Theorem 6M(4)ac8 9072  dfac5 8709
[Enderton] p. 159Theorem 6Qunictb 9151
[Enderton] p. 164Exampleinfdif 8789
[Enderton] p. 168Definitiondf-po 4853
[Enderton] p. 192Theorem 7M(a)oneli 5637
[Enderton] p. 192Theorem 7M(b)ontr1 5576
[Enderton] p. 192Theorem 7M(c)onirri 5636
[Enderton] p. 193Corollary 7N(b)0elon 5583
[Enderton] p. 193Corollary 7N(c)onsuci 6805
[Enderton] p. 193Corollary 7N(d)ssonunii 6754
[Enderton] p. 194Remarkonprc 6751
[Enderton] p. 194Exercise 16suc11 5633
[Enderton] p. 197Definitiondf-card 8523
[Enderton] p. 197Theorem 7Pcarden 9127
[Enderton] p. 200Exercise 25tfis 6821
[Enderton] p. 202Lemma 7Tr1tr 8397
[Enderton] p. 202Definitiondf-r1 8385
[Enderton] p. 202Theorem 7Qr1val1 8407
[Enderton] p. 204Theorem 7V(b)rankval4 8488
[Enderton] p. 206Theorem 7X(b)en2lp 8268
[Enderton] p. 207Exercise 30rankpr 8478  rankprb 8472  rankpw 8464  rankpwi 8444  rankuniss 8487
[Enderton] p. 207Exercise 34opthreg 8273
[Enderton] p. 208Exercise 35suc11reg 8274
[Enderton] p. 212Definition of alephalephval3 8691
[Enderton] p. 213Theorem 8A(a)alephord2 8657
[Enderton] p. 213Theorem 8A(b)cardalephex 8671
[Enderton] p. 218Theorem Schema 8Eonfununi 7200
[Enderton] p. 222Definition of kardkarden 8516  kardex 8515
[Enderton] p. 238Theorem 8Roeoa 7439
[Enderton] p. 238Theorem 8Soeoe 7441
[Enderton] p. 240Exercise 25oarec 7404
[Enderton] p. 257Definition of cofinalitycflm 8830
[FaureFrolicher] p. 57Definition 3.1.9mreexd 16015
[FaureFrolicher] p. 83Definition 4.1.1df-mri 15961
[FaureFrolicher] p. 83Proposition 4.1.3acsfiindd 16890  mrieqv2d 16012  mrieqvd 16011
[FaureFrolicher] p. 84Lemma 4.1.5mreexmrid 16016
[FaureFrolicher] p. 86Proposition 4.2.1mreexexd 16021  mreexexlem2d 16018
[FaureFrolicher] p. 87Theorem 4.2.2acsexdimd 16896  mreexfidimd 16024
[Frege1879] p. 11Statementdf3or2 36961
[Frege1879] p. 12Statementdf3an2 36962  dfxor4 36959  dfxor5 36960
[Frege1879] p. 26Axiom 1ax-frege1 36986
[Frege1879] p. 26Axiom 2ax-frege2 36987
[Frege1879] p. 26Proposition 1ax-1 6
[Frege1879] p. 26Proposition 2ax-2 7
[Frege1879] p. 29Proposition 3frege3 36991
[Frege1879] p. 31Proposition 4frege4 36995
[Frege1879] p. 32Proposition 5frege5 36996
[Frege1879] p. 33Proposition 6frege6 37002
[Frege1879] p. 34Proposition 7frege7 37004
[Frege1879] p. 35Axiom 8ax-frege8 37005  axfrege8 37003
[Frege1879] p. 35Proposition 8pm2.04 87  wl-pm2.04 32275
[Frege1879] p. 35Proposition 9frege9 37008
[Frege1879] p. 36Proposition 10frege10 37016
[Frege1879] p. 36Proposition 11frege11 37010
[Frege1879] p. 37Proposition 12frege12 37009
[Frege1879] p. 37Proposition 13frege13 37018
[Frege1879] p. 37Proposition 14frege14 37019
[Frege1879] p. 38Proposition 15frege15 37022
[Frege1879] p. 38Proposition 16frege16 37012
[Frege1879] p. 39Proposition 17frege17 37017
[Frege1879] p. 39Proposition 18frege18 37014
[Frege1879] p. 39Proposition 19frege19 37020
[Frege1879] p. 40Proposition 20frege20 37024
[Frege1879] p. 40Proposition 21frege21 37023
[Frege1879] p. 41Proposition 22frege22 37015
[Frege1879] p. 42Proposition 23frege23 37021
[Frege1879] p. 42Proposition 24frege24 37011
[Frege1879] p. 42Proposition 25frege25 37013  rp-frege25 37001
[Frege1879] p. 42Proposition 26frege26 37006
[Frege1879] p. 43Axiom 28ax-frege28 37026
[Frege1879] p. 43Proposition 27frege27 37007
[Frege1879] p. 43Proposition 28con3 147
[Frege1879] p. 43Proposition 29frege29 37027
[Frege1879] p. 44Axiom 31ax-frege31 37030  axfrege31 37029
[Frege1879] p. 44Proposition 30frege30 37028
[Frege1879] p. 44Proposition 31notnotr 123
[Frege1879] p. 44Proposition 32frege32 37031
[Frege1879] p. 44Proposition 33frege33 37032
[Frege1879] p. 45Proposition 34frege34 37033
[Frege1879] p. 45Proposition 35frege35 37034
[Frege1879] p. 45Proposition 36frege36 37035
[Frege1879] p. 46Proposition 37frege37 37036
[Frege1879] p. 46Proposition 38frege38 37037
[Frege1879] p. 46Proposition 39frege39 37038
[Frege1879] p. 46Proposition 40frege40 37039
[Frege1879] p. 47Axiom 41ax-frege41 37041  axfrege41 37040
[Frege1879] p. 47Proposition 41notnot 134
[Frege1879] p. 47Proposition 42frege42 37042
[Frege1879] p. 47Proposition 43frege43 37043
[Frege1879] p. 47Proposition 44frege44 37044
[Frege1879] p. 47Proposition 45frege45 37045
[Frege1879] p. 48Proposition 46frege46 37046
[Frege1879] p. 48Proposition 47frege47 37047
[Frege1879] p. 49Proposition 48frege48 37048
[Frege1879] p. 49Proposition 49frege49 37049
[Frege1879] p. 49Proposition 50frege50 37050
[Frege1879] p. 50Axiom 52ax-frege52a 37053  ax-frege52c 37084  frege52aid 37054  frege52b 37085
[Frege1879] p. 50Axiom 54ax-frege54a 37058  ax-frege54c 37088  frege54b 37089
[Frege1879] p. 50Proposition 51frege51 37051
[Frege1879] p. 50Proposition 52dfsbcq 3308
[Frege1879] p. 50Proposition 53frege53a 37056  frege53aid 37055  frege53b 37086  frege53c 37110
[Frege1879] p. 50Proposition 54biid 249  eqid 2514
[Frege1879] p. 50Proposition 55frege55a 37064  frege55aid 37061  frege55b 37093  frege55c 37114  frege55cor1a 37065  frege55lem2a 37063  frege55lem2b 37092  frege55lem2c 37113
[Frege1879] p. 50Proposition 56frege56a 37067  frege56aid 37066  frege56b 37094  frege56c 37115
[Frege1879] p. 51Axiom 58ax-frege58a 37071  ax-frege58b 37097  frege58bid 37098  frege58c 37117
[Frege1879] p. 51Proposition 57frege57a 37069  frege57aid 37068  frege57b 37095  frege57c 37116
[Frege1879] p. 51Proposition 58spsbc 3319
[Frege1879] p. 51Proposition 59frege59a 37073  frege59b 37100  frege59c 37118
[Frege1879] p. 52Proposition 60frege60a 37074  frege60b 37101  frege60c 37119
[Frege1879] p. 52Proposition 61frege61a 37075  frege61b 37102  frege61c 37120
[Frege1879] p. 52Proposition 62frege62a 37076  frege62b 37103  frege62c 37121
[Frege1879] p. 52Proposition 63frege63a 37077  frege63b 37104  frege63c 37122
[Frege1879] p. 53Proposition 64frege64a 37078  frege64b 37105  frege64c 37123
[Frege1879] p. 53Proposition 65frege65a 37079  frege65b 37106  frege65c 37124
[Frege1879] p. 54Proposition 66frege66a 37080  frege66b 37107  frege66c 37125
[Frege1879] p. 54Proposition 67frege67a 37081  frege67b 37108  frege67c 37126
[Frege1879] p. 54Proposition 68frege68a 37082  frege68b 37109  frege68c 37127
[Frege1879] p. 55Definition 69dffrege69 37128
[Frege1879] p. 58Proposition 70frege70 37129
[Frege1879] p. 59Proposition 71frege71 37130
[Frege1879] p. 59Proposition 72frege72 37131
[Frege1879] p. 59Proposition 73frege73 37132
[Frege1879] p. 60Definition 76dffrege76 37135
[Frege1879] p. 60Proposition 74frege74 37133
[Frege1879] p. 60Proposition 75frege75 37134
[Frege1879] p. 62Proposition 77frege77 37136  frege77d 36939
[Frege1879] p. 63Proposition 78frege78 37137
[Frege1879] p. 63Proposition 79frege79 37138
[Frege1879] p. 63Proposition 80frege80 37139
[Frege1879] p. 63Proposition 81frege81 37140  frege81d 36940
[Frege1879] p. 64Proposition 82frege82 37141
[Frege1879] p. 65Proposition 83frege83 37142  frege83d 36941
[Frege1879] p. 65Proposition 84frege84 37143
[Frege1879] p. 66Proposition 85frege85 37144
[Frege1879] p. 66Proposition 86frege86 37145
[Frege1879] p. 66Proposition 87frege87 37146  frege87d 36943
[Frege1879] p. 67Proposition 88frege88 37147
[Frege1879] p. 68Proposition 89frege89 37148
[Frege1879] p. 68Proposition 90frege90 37149
[Frege1879] p. 68Proposition 91frege91 37150  frege91d 36944
[Frege1879] p. 69Proposition 92frege92 37151
[Frege1879] p. 70Proposition 93frege93 37152
[Frege1879] p. 70Proposition 94frege94 37153
[Frege1879] p. 70Proposition 95frege95 37154
[Frege1879] p. 71Definition 99dffrege99 37158
[Frege1879] p. 71Proposition 96frege96 37155  frege96d 36942
[Frege1879] p. 71Proposition 97frege97 37156  frege97d 36945
[Frege1879] p. 71Proposition 98frege98 37157  frege98d 36946
[Frege1879] p. 72Proposition 100frege100 37159
[Frege1879] p. 72Proposition 101frege101 37160
[Frege1879] p. 72Proposition 102frege102 37161  frege102d 36947
[Frege1879] p. 73Proposition 103frege103 37162
[Frege1879] p. 73Proposition 104frege104 37163
[Frege1879] p. 73Proposition 105frege105 37164
[Frege1879] p. 73Proposition 106frege106 37165  frege106d 36948
[Frege1879] p. 74Proposition 107frege107 37166
[Frege1879] p. 74Proposition 108frege108 37167  frege108d 36949
[Frege1879] p. 74Proposition 109frege109 37168  frege109d 36950
[Frege1879] p. 75Proposition 110frege110 37169
[Frege1879] p. 75Proposition 111frege111 37170  frege111d 36952
[Frege1879] p. 76Proposition 112frege112 37171
[Frege1879] p. 76Proposition 113frege113 37172
[Frege1879] p. 76Proposition 114frege114 37173  frege114d 36951
[Frege1879] p. 77Definition 115dffrege115 37174
[Frege1879] p. 77Proposition 116frege116 37175
[Frege1879] p. 78Proposition 117frege117 37176
[Frege1879] p. 78Proposition 118frege118 37177
[Frege1879] p. 78Proposition 119frege119 37178
[Frege1879] p. 78Proposition 120frege120 37179
[Frege1879] p. 79Proposition 121frege121 37180
[Frege1879] p. 79Proposition 122frege122 37181  frege122d 36953
[Frege1879] p. 79Proposition 123frege123 37182
[Frege1879] p. 80Proposition 124frege124 37183  frege124d 36954
[Frege1879] p. 81Proposition 125frege125 37184
[Frege1879] p. 81Proposition 126frege126 37185  frege126d 36955
[Frege1879] p. 82Proposition 127frege127 37186
[Frege1879] p. 83Proposition 128frege128 37187
[Frege1879] p. 83Proposition 129frege129 37188  frege129d 36956
[Frege1879] p. 84Proposition 130frege130 37189
[Frege1879] p. 85Proposition 131frege131 37190  frege131d 36957
[Frege1879] p. 86Proposition 132frege132 37191
[Frege1879] p. 86Proposition 133frege133 37192  frege133d 36958
[Fremlin1] p. 13Definition 111G (b)df-salgen 39103
[Fremlin1] p. 13Definition 111G (d)borelmbl 39420
[Fremlin1] p. 13Proposition 111G (b)salgenss 39124
[Fremlin1] p. 14Definition 112Aismea 39238
[Fremlin1] p. 15Remark 112B (d)psmeasure 39258
[Fremlin1] p. 15Property 112C (a)meadjun 39249  meadjunre 39263
[Fremlin1] p. 15Property 112C (b)meassle 39250
[Fremlin1] p. 15Property 112C (c)meaunle 39251
[Fremlin1] p. 16Property 112C (d)iundjiun 39247  meaiunle 39256  meaiunlelem 39255
[Fremlin1] p. 16Proposition 112C (e)meaiuninc 39268  meaiuninc2 39269  meaiuninclem 39267
[Fremlin1] p. 16Proposition 112C (f)meaiininc 39271  meaiininc2 39272  meaiininclem 39270
[Fremlin1] p. 19Theorem 113Ccaragen0 39290  caragendifcl 39298  caratheodory 39312  omelesplit 39302
[Fremlin1] p. 19Definition 113Aisome 39278  isomennd 39315  isomenndlem 39314
[Fremlin1] p. 19Remark 113B (c)omeunle 39300
[Fremlin1] p. 19Definition 112Dfcaragencmpl 39319  voncmpl 39405
[Fremlin1] p. 19Definition 113A (ii)omessle 39282
[Fremlin1] p. 20Theorem 113Ccarageniuncl 39307  carageniuncllem1 39305  carageniuncllem2 39306  caragenuncl 39297  caragenuncllem 39296  caragenunicl 39308
[Fremlin1] p. 21Remark 113Dcaragenel2d 39316
[Fremlin1] p. 21Theorem 113Ccaratheodorylem1 39310  caratheodorylem2 39311
[Fremlin1] p. 21Exercise 113Xacaragencmpl 39319
[Fremlin1] p. 23Lemma 114Bhoidmv1le 39378  hoidmv1lelem1 39375  hoidmv1lelem2 39376  hoidmv1lelem3 39377
[Fremlin1] p. 25Definition 114Eisvonmbl 39422
[Fremlin1] p. 29Lemma 115Bhoidmv1le 39378  hoidmvle 39384  hoidmvlelem1 39379  hoidmvlelem2 39380  hoidmvlelem3 39381  hoidmvlelem4 39382  hoidmvlelem5 39383  hsphoidmvle2 39369  hsphoif 39360  hsphoival 39363
[Fremlin1] p. 29Definition 1135 (b)hoicvr 39332
[Fremlin1] p. 29Definition 115A (b)hoicvrrex 39340
[Fremlin1] p. 29Definition 115A (c)hoidmv0val 39367  hoidmvn0val 39368  hoidmvval 39361  hoidmvval0 39371  hoidmvval0b 39374
[Fremlin1] p. 30Lemma 115Bhoiprodp1 39372  hsphoidmvle 39370
[Fremlin1] p. 30Definition 115Cdf-ovoln 39321  df-voln 39323
[Fremlin1] p. 30Proposition 115D (a)dmovn 39388  ovn0 39350  ovn0lem 39349  ovnf 39347  ovnome 39357  ovnssle 39345  ovnsslelem 39344  ovnsupge0 39341
[Fremlin1] p. 30Proposition 115D (b)ovnhoi 39387  ovnhoilem1 39385  ovnhoilem2 39386  vonhoi 39451
[Fremlin1] p. 31Lemma 115Fhoidifhspdmvle 39404  hoidifhspf 39402  hoidifhspval 39392  hoidifhspval2 39399  hoidifhspval3 39403  hspmbl 39413  hspmbllem1 39410  hspmbllem2 39411  hspmbllem3 39412
[Fremlin1] p. 31Definition 115Evoncmpl 39405  vonmea 39358
[Fremlin1] p. 31Proposition 115D (a)(iv)ovnsubadd 39356  ovnsubadd2 39430  ovnsubadd2lem 39429  ovnsubaddlem1 39354  ovnsubaddlem2 39355
[Fremlin1] p. 32Proposition 115G (a)hoimbl 39415  hoimbl2 39449  hoimbllem 39414  hspdifhsp 39400  opnvonmbl 39418  opnvonmbllem2 39417
[Fremlin1] p. 32Proposition 115G (b)borelmbl 39420
[Fremlin1] p. 32Proposition 115G (c)iccvonmbl 39464  iccvonmbllem 39463  ioovonmbl 39462
[Fremlin1] p. 32Proposition 115G (d)vonicc 39470  vonicclem2 39469  vonioo 39467  vonioolem2 39466  vonn0icc 39473  vonn0icc2 39477  vonn0ioo 39472  vonn0ioo2 39475
[Fremlin1] p. 32Proposition 115G (e)ctvonmbl 39474  snvonmbl 39471  vonct 39478  vonsn 39476
[Fremlin1] p. 35Lemma 121Asubsalsal 39147
[Fremlin1] p. 35Lemma 121A (iii)subsaliuncl 39146  subsaliuncllem 39145
[Fremlin1] p. 35Proposition 121Bsalpreimagtge 39505  salpreimalegt 39491  salpreimaltle 39506
[Fremlin1] p. 35Proposition 121B (i)issmf 39508  issmff 39514  issmflem 39507
[Fremlin1] p. 35Proposition 121B (ii)issmfle 39526  issmflelem 39525  issmfltle 39516
[Fremlin1] p. 35Proposition 121B (iii)issmfgt 39537  issmfgtlem 39536
[Fremlin1] p. 36Definition 121Cdf-smblfn 39481  issmf 39508  issmff 39514  issmfge 39550  issmfgelem 39549  issmfgt 39537  issmfgtlem 39536  issmfle 39526  issmflelem 39525  issmflem 39507
[Fremlin1] p. 36Proposition 121Bsalpreimagelt 39489  salpreimagtlt 39510  salpreimalelt 39509
[Fremlin1] p. 36Proposition 121B (iv)issmfge 39550  issmfgelem 39549
[Fremlin1] p. 36Proposition 121D (a)bormflebmf 39534
[Fremlin1] p. 36Proposition 121D (b)cnfrrnsmf 39532  cnfsmf 39521
[Fremlin1] p. 36Proposition 121D (c)decsmf 39547  decsmflem 39546  incsmf 39523  incsmflem 39522
[Fremlin1] p. 37Proposition 121E (a)pimconstlt0 39485  pimconstlt1 39486  smfconst 39530
[Fremlin1] p. 37Proposition 121E (b)smfadd 39545  smfaddlem1 39543  smfaddlem2 39544
[Fremlin1] p. 37Proposition 121E (c)smfmulc1 39575
[Fremlin1] p. 37Proposition 121E (d)smfmul 39574  smfmullem1 39570  smfmullem2 39571  smfmullem3 39572  smfmullem4 39573
[Fremlin1] p. 37Proposition 121E (e)smfdiv 39576
[Fremlin1] p. 37Proposition 121E (f)smfpimbor1 39579  smfpimbor1lem2 39578
[Fremlin1] p. 37Proposition 121E (g)smfco 39581
[Fremlin1] p. 37Proposition 121E (h)smfres 39569
[Fremlin1] p. 38Proposition 121E (e)smfrec 39568
[Fremlin1] p. 38Proposition 121E (f)smfpimbor1lem1 39577  smfresal 39567
[Fremlin1] p. 38Proposition 121F (a)smflim 39557  smflimlem1 39551  smflimlem2 39552  smflimlem3 39553  smflimlem4 39554  smflimlem5 39555  smflimlem6 39556
[Fremlin1] p. 39Remark 121Gsmflim 39557
[Fremlin1] p. 80Definition 135E (b)df-smblfn 39481
[Fremlin5] p. 193Proposition 563Gbnulmbl2 22987
[Fremlin5] p. 213Lemma 565Cauniioovol 23029
[Fremlin5] p. 214Lemma 565Cauniioombl 23039
[Fremlin5] p. 218Lemma 565Ibftc1anclem6 32535
[Fremlin5] p. 220Theorem 565Maftc1anc 32538
[FreydScedrov] p. 283Axiom of Infinityax-inf 8293  inf1 8277  inf2 8278
[Gleason] p. 117Proposition 9-2.1df-enq 9487  enqer 9497
[Gleason] p. 117Proposition 9-2.2df-1nq 9492  df-nq 9488
[Gleason] p. 117Proposition 9-2.3df-plpq 9484  df-plq 9490
[Gleason] p. 119Proposition 9-2.4caovmo 6644  df-mpq 9485  df-mq 9491
[Gleason] p. 119Proposition 9-2.5df-rq 9493
[Gleason] p. 119Proposition 9-2.6ltexnq 9551
[Gleason] p. 120Proposition 9-2.6(i)halfnq 9552  ltbtwnnq 9554
[Gleason] p. 120Proposition 9-2.6(ii)ltanq 9547
[Gleason] p. 120Proposition 9-2.6(iii)ltmnq 9548
[Gleason] p. 120Proposition 9-2.6(iv)ltrnq 9555
[Gleason] p. 121Definition 9-3.1df-np 9557
[Gleason] p. 121Definition 9-3.1 (ii)prcdnq 9569
[Gleason] p. 121Definition 9-3.1(iii)prnmax 9571
[Gleason] p. 122Definitiondf-1p 9558
[Gleason] p. 122Remark (1)prub 9570
[Gleason] p. 122Lemma 9-3.4prlem934 9609
[Gleason] p. 122Proposition 9-3.2df-ltp 9561
[Gleason] p. 122Proposition 9-3.3ltsopr 9608  psslinpr 9607  supexpr 9630  suplem1pr 9628  suplem2pr 9629
[Gleason] p. 123Proposition 9-3.5addclpr 9594  addclprlem1 9592  addclprlem2 9593  df-plp 9559
[Gleason] p. 123Proposition 9-3.5(i)addasspr 9598
[Gleason] p. 123Proposition 9-3.5(ii)addcompr 9597
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 9610
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 9619  ltexprlem1 9612  ltexprlem2 9613  ltexprlem3 9614  ltexprlem4 9615  ltexprlem5 9616  ltexprlem6 9617  ltexprlem7 9618
[Gleason] p. 123Proposition 9-3.5(v)ltapr 9621  ltaprlem 9620
[Gleason] p. 123Proposition 9-3.5(vi)addcanpr 9622
[Gleason] p. 124Lemma 9-3.6prlem936 9623
[Gleason] p. 124Proposition 9-3.7df-mp 9560  mulclpr 9596  mulclprlem 9595  reclem2pr 9624
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 9605
[Gleason] p. 124Proposition 9-3.7(i)mulasspr 9600
[Gleason] p. 124Proposition 9-3.7(ii)mulcompr 9599
[Gleason] p. 124Proposition 9-3.7(iii)distrpr 9604
[Gleason] p. 124Proposition 9-3.7(v)recexpr 9627  reclem3pr 9625  reclem4pr 9626
[Gleason] p. 126Proposition 9-4.1df-enr 9631  enrer 9640
[Gleason] p. 126Proposition 9-4.2df-0r 9636  df-1r 9637  df-nr 9632
[Gleason] p. 126Proposition 9-4.3df-mr 9634  df-plr 9633  negexsr 9677  recexsr 9682  recexsrlem 9678
[Gleason] p. 127Proposition 9-4.4df-ltr 9635
[Gleason] p. 130Proposition 10-1.3creui 10769  creur 10768  cru 10766
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 9763  axcnre 9739
[Gleason] p. 132Definition 10-3.1crim 13560  crimd 13677  crimi 13638  crre 13559  crred 13676  crrei 13637
[Gleason] p. 132Definition 10-3.2remim 13562  remimd 13643
[Gleason] p. 133Definition 10.36absval2 13729  absval2d 13889  absval2i 13841
[Gleason] p. 133Proposition 10-3.4(a)cjadd 13586  cjaddd 13665  cjaddi 13633
[Gleason] p. 133Proposition 10-3.4(c)cjmul 13587  cjmuld 13666  cjmuli 13634
[Gleason] p. 133Proposition 10-3.4(e)cjcj 13585  cjcjd 13644  cjcji 13616
[Gleason] p. 133Proposition 10-3.4(f)cjre 13584  cjreb 13568  cjrebd 13647  cjrebi 13619  cjred 13671  rere 13567  rereb 13565  rerebd 13646  rerebi 13618  rered 13669
[Gleason] p. 133Proposition 10-3.4(h)addcj 13593  addcjd 13657  addcji 13628
[Gleason] p. 133Proposition 10-3.7(a)absval 13683
[Gleason] p. 133Proposition 10-3.7(b)abscj 13724  abscjd 13894  abscji 13845
[Gleason] p. 133Proposition 10-3.7(c)abs00 13734  abs00d 13890  abs00i 13842  absne0d 13891
[Gleason] p. 133Proposition 10-3.7(d)releabs 13766  releabsd 13895  releabsi 13846
[Gleason] p. 133Proposition 10-3.7(f)absmul 13739  absmuld 13898  absmuli 13848
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 13727  sqabsaddi 13849
[Gleason] p. 133Proposition 10-3.7(h)abstri 13775  abstrid 13900  abstrii 13852
[Gleason] p. 134Definition 10-4.10exp0e1 12594  df-exp 12590  exp0 12593  expp1 12596  expp1d 12738
[Gleason] p. 135Proposition 10-4.2(a)cxpadd 24113  cxpaddd 24151  expadd 12631  expaddd 12739  expaddz 12633
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 24122  cxpmuld 24168  expmul 12634  expmuld 12740  expmulz 12635
[Gleason] p. 135Proposition 10-4.2(c)mulcxp 24119  mulcxpd 24162  mulexp 12628  mulexpd 12752  mulexpz 12629
[Gleason] p. 140Exercise 1znnen 14647
[Gleason] p. 141Definition 11-2.1fzval 12066
[Gleason] p. 168Proposition 12-2.1(a)climadd 14074  rlimadd 14085  rlimdiv 14088
[Gleason] p. 168Proposition 12-2.1(b)climsub 14076  rlimsub 14086
[Gleason] p. 168Proposition 12-2.1(c)climmul 14075  rlimmul 14087
[Gleason] p. 171Corollary 12-2.2climmulc2 14079
[Gleason] p. 172Corollary 12-2.5climrecl 14026
[Gleason] p. 172Proposition 12-2.4(c)climabs 14046  climcj 14047  climim 14049  climre 14048  rlimabs 14051  rlimcj 14052  rlimim 14054  rlimre 14053
[Gleason] p. 173Definition 12-3.1df-ltxr 9833  df-xr 9832  ltxr 11693
[Gleason] p. 175Definition 12-4.1df-limsup 13908  limsupval 13913
[Gleason] p. 180Theorem 12-5.1climsup 14112
[Gleason] p. 180Theorem 12-5.3caucvg 14124  caucvgb 14125  caucvgr 14120  climcau 14113
[Gleason] p. 182Exercise 3cvgcmp 14256
[Gleason] p. 182Exercise 4cvgrat 14321
[Gleason] p. 195Theorem 13-2.12abs1m 13780
[Gleason] p. 217Lemma 13-4.1btwnzge0 12358
[Gleason] p. 223Definition 14-1.1df-met 19463
[Gleason] p. 223Definition 14-1.1(a)met0 21858  xmet0 21857
[Gleason] p. 223Definition 14-1.1(b)metgt0 21874
[Gleason] p. 223Definition 14-1.1(c)metsym 21865
[Gleason] p. 223Definition 14-1.1(d)mettri 21867  mstri 21984  xmettri 21866  xmstri 21983
[Gleason] p. 225Definition 14-1.5xpsmet 21897
[Gleason] p. 230Proposition 14-2.6txlm 21162
[Gleason] p. 240Theorem 14-4.3metcnp4 22780
[Gleason] p. 240Proposition 14-4.2metcnp3 22055
[Gleason] p. 243Proposition 14-4.16addcn 22397  addcn2 14036  mulcn 22399  mulcn2 14038  subcn 22398  subcn2 14037
[Gleason] p. 295Remarkbcval3 12822  bcval4 12823
[Gleason] p. 295Equation 2bcpasc 12837
[Gleason] p. 295Definition of binomial coefficientbcval 12820  df-bc 12819
[Gleason] p. 296Remarkbcn0 12826  bcnn 12828
[Gleason] p. 296Theorem 15-2.8binom 14268
[Gleason] p. 308Equation 2ef0 14527
[Gleason] p. 308Equation 3efcj 14528
[Gleason] p. 309Corollary 15-4.3efne0 14533
[Gleason] p. 309Corollary 15-4.4efexp 14537
[Gleason] p. 310Equation 14sinadd 14600
[Gleason] p. 310Equation 15cosadd 14601
[Gleason] p. 311Equation 17sincossq 14612
[Gleason] p. 311Equation 18cosbnd 14617  sinbnd 14616
[Gleason] p. 311Lemma 15-4.7sqeqor 12707  sqeqori 12705
[Gleason] p. 311Definition of pidf-pi 14509
[Godowski] p. 730Equation SFgoeqi 28305
[GodowskiGreechie] p. 249Equation IV3oai 27700
[Golan] p. 1Remarksrgisid 18256
[Golan] p. 1Definitiondf-srg 18234
[Golan] p. 149Definitiondf-slmd 28882
[GramKnuthPat], p. 47Definition 2.42df-fwddif 31272
[Gratzer] p. 23Section 0.6df-mre 15959
[Gratzer] p. 27Section 0.6df-mri 15961
[Hall] p. 1Section 1.1df-asslaw 41706  df-cllaw 41704  df-comlaw 41705
[Hall] p. 2Section 1.2df-clintop 41718
[Hall] p. 7Section 1.3df-sgrp2 41739
[Halmos] p. 31Theorem 17.3riesz1 28097  riesz2 28098
[Halmos] p. 41Definition of Hermitianhmopadj2 27973
[Halmos] p. 42Definition of projector orderingpjordi 28205
[Halmos] p. 43Theorem 26.1elpjhmop 28217  elpjidm 28216  pjnmopi 28180
[Halmos] p. 44Remarkpjinormi 27719  pjinormii 27708
[Halmos] p. 44Theorem 26.2elpjch 28221  pjrn 27739  pjrni 27734  pjvec 27728
[Halmos] p. 44Theorem 26.3pjnorm2 27759
[Halmos] p. 44Theorem 26.4hmopidmpj 28186  hmopidmpji 28184
[Halmos] p. 45Theorem 27.1pjinvari 28223
[Halmos] p. 45Theorem 27.3pjoci 28212  pjocvec 27729
[Halmos] p. 45Theorem 27.4pjorthcoi 28201
[Halmos] p. 48Theorem 29.2pjssposi 28204
[Halmos] p. 48Theorem 29.3pjssdif1i 28207  pjssdif2i 28206
[Halmos] p. 50Definition of spectrumdf-spec 27887
[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 1700
[Hatcher] p. 25Definitiondf-phtpc 22523  df-phtpy 22502
[Hatcher] p. 26Definitiondf-pco 22537  df-pi1 22540
[Hatcher] p. 26Proposition 1.2phtpcer 22526
[Hatcher] p. 26Proposition 1.3pi1grp 22582
[Hefferon] p. 240Definition 3.12df-dmat 20016  df-dmatalt 42073
[Helfgott] p. 2Theoremtgoldbach 40127
[Helfgott] p. 4Corollary 1.1wtgoldbnnsum4prm 40113
[Helfgott] p. 4Section 1.2.2ax-hgprmladder 40123  bgoldbtbnd 40120  bgoldbtbnd 40120  tgblthelfgott 40124
[Helfgott] p. 70Section 7.4ax-tgoldbachgt 40126
[Herstein] p. 54Exercise 28df-grpo 26470
[Herstein] p. 55Lemma 2.2.1(a)grpideu 17146  grpoideu 26486  mndideu 17017
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 17169  grpoinveu 26496
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 17195  grpo2inv 26508
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 17206  grpoinvop 26510
[Herstein] p. 57Exercise 1dfgrp3e 17228
[Hitchcock] p. 5Rule A3mptnan 1683
[Hitchcock] p. 5Rule A4mptxor 1684
[Hitchcock] p. 5Rule A5mtpxor 1686
[Holland] p. 1519Theorem 2sumdmdi 28452
[Holland] p. 1520Lemma 5cdj1i 28465  cdj3i 28473  cdj3lem1 28466  cdjreui 28464
[Holland] p. 1524Lemma 7mddmdin0i 28463
[Holland95] p. 13Theorem 3.6hlathil 36146
[Holland95] p. 14Line 15hgmapvs 36076
[Holland95] p. 14Line 16hdmaplkr 36098
[Holland95] p. 14Line 17hdmapellkr 36099
[Holland95] p. 14Line 19hdmapglnm2 36096
[Holland95] p. 14Line 20hdmapip0com 36102
[Holland95] p. 14Theorem 3.6hdmapevec2 36021
[Holland95] p. 14Lines 24 and 25hdmapoc 36116
[Holland95] p. 204Definition of involutiondf-srng 18574
[Holland95] p. 212Definition of subspacedf-psubsp 33682
[Holland95] p. 214Lemma 3.3lclkrlem2v 35710
[Holland95] p. 214Definition 3.2df-lpolN 35663
[Holland95] p. 214Definition of nonsingularpnonsingN 34112
[Holland95] p. 215Lemma 3.3(1)dihoml4 35559  poml4N 34132
[Holland95] p. 215Lemma 3.3(2)dochexmid 35650  pexmidALTN 34157  pexmidN 34148
[Holland95] p. 218Theorem 3.6lclkr 35715
[Holland95] p. 218Definition of dual vector spacedf-ldual 33304  ldualset 33305
[Holland95] p. 222Item 1df-lines 33680  df-pointsN 33681
[Holland95] p. 222Item 2df-polarityN 34082
[Holland95] p. 223Remarkispsubcl2N 34126  omllaw4 33426  pol1N 34089  polcon3N 34096
[Holland95] p. 223Definitiondf-psubclN 34114
[Holland95] p. 223Equation for polaritypolval2N 34085
[Hughes] p. 44Equation 1.21bax-his3 27114
[Hughes] p. 47Definition of projection operatordfpjop 28214
[Hughes] p. 49Equation 1.30eighmre 27995  eigre 27867  eigrei 27866
[Hughes] p. 49Equation 1.31eighmorth 27996  eigorth 27870  eigorthi 27869
[Hughes] p. 137Remark (ii)eigposi 27868
[Huneke] p. 1Claim 1frgrancvvdeq 26308  frgrancvvdgeq 26309  frgrncvvdeq 41572
[Huneke] p. 1Statement 1frgrancvvdeqlemA 26303  frgrncvvdeqlemA 41568
[Huneke] p. 1Statement 2frgrancvvdeqlemB 26304  frgrncvvdeqlemB 41569
[Huneke] p. 1Statement 3frgrancvvdeqlemC 26305  frgrncvvdeqlemC 41570
[Huneke] p. 2Claim 2frgraregorufr 26319  frgraregorufr0 26318  frgraregorufrg 26338  frgrregorufr 41582  frgrregorufr0 41581  frgrregorufrg 41597
[Huneke] p. 2Claim 3frghash2spot 26329  frgregordn0 26336  frgrhash2wsp 41589  frrusgraord 26337  frrusgrord 41596  frrusgrord0 41595
[Huneke] p. 2Statement 4frgrawopreglem4 26313  frgrwopreglem4 41576
[Huneke] p. 2Statement 5frgrawopreg1 26316  frgrawopreg2 26317  frgrwopreg1 41579  frgrwopreg2 41580
[Huneke] p. 2Statement 6frgrawopreglem5 26314  frgrwopreglem5 41577
[Huneke] p. 2Statement 7fusgreghash2wspv 41591  usgreghash2spotv 26332
[Huneke] p. 2Statement 8fusgreghash2wsp 41594  usgreghash2spot 26335
[Huneke] p. 2Statement 9av-numclwwlk1 41620  av-numclwwlk8 41638  clwlkndivn 26119  clwlksndivn 41371  numclwwlk1 26364  numclwwlk8 26381
[Huneke] p. 2Definition 3frgrawopreglem1 26310  frgrwopreglem1 41573
[Huneke] p. 2Definition 4df-clwlk 26017  df-clwlks 41069
[Huneke] p. 2Definition 5av-numclwwlkovf 41603  numclwwlkovf 26347
[Huneke] p. 2Definition 6av-numclwwlkovg 41610  numclwwlkovg 26353
[Huneke] p. 2Definition 7av-numclwwlkovh 41623  numclwwlkovh 26367
[Huneke] p. 2Statement 10av-numclwwlk2 41629  numclwwlk2 26373
[Huneke] p. 2Statement 11rusgranumwlk 26223  rusgranumwlkg 26224  rusgrnumwlkg 41272
[Huneke] p. 2Statement 12av-numclwwlk3 41631  numclwwlk3 26375
[Huneke] p. 2Statement 13av-numclwwlk5 41634  numclwwlk5 26378
[Huneke] p. 2Statement 14av-numclwwlk7 41637  numclwwlk7 26380
[Indrzejczak] p. 33Definition ` `Enatded 26391  natded 26391
[Indrzejczak] p. 33Definition ` `Inatded 26391
[Indrzejczak] p. 34Definition ` `Enatded 26391  natded 26391
[Indrzejczak] p. 34Definition ` `Inatded 26391
[Jech] p. 4Definition of classcv 1473  cvjust 2509
[Jech] p. 42Lemma 6.1alephexp1 9155
[Jech] p. 42Equation 6.1alephadd 9153  alephmul 9154
[Jech] p. 43Lemma 6.2infmap 9152  infmap2 8798
[Jech] p. 71Lemma 9.3jech9.3 8435
[Jech] p. 72Equation 9.3scott0 8507  scottex 8506
[Jech] p. 72Exercise 9.1rankval4 8488
[Jech] p. 72Scheme "Collection Principle"cp 8512
[Jech] p. 78Noteopthprc 4983
[JonesMatijasevic] p. 694Definition 2.3rmxyval 36373
[JonesMatijasevic] p. 695Lemma 2.15jm2.15nn0 36463
[JonesMatijasevic] p. 695Lemma 2.16jm2.16nn0 36464
[JonesMatijasevic] p. 695Equation 2.7rmxadd 36385
[JonesMatijasevic] p. 695Equation 2.8rmyadd 36389
[JonesMatijasevic] p. 695Equation 2.9rmxp1 36390  rmyp1 36391
[JonesMatijasevic] p. 695Equation 2.10rmxm1 36392  rmym1 36393
[JonesMatijasevic] p. 695Equation 2.11rmx0 36383  rmx1 36384  rmxluc 36394
[JonesMatijasevic] p. 695Equation 2.12rmy0 36387  rmy1 36388  rmyluc 36395
[JonesMatijasevic] p. 695Equation 2.13rmxdbl 36397
[JonesMatijasevic] p. 695Equation 2.14rmydbl 36398
[JonesMatijasevic] p. 696Lemma 2.17jm2.17a 36420  jm2.17b 36421  jm2.17c 36422
[JonesMatijasevic] p. 696Lemma 2.19jm2.19 36453
[JonesMatijasevic] p. 696Lemma 2.20jm2.20nn 36457
[JonesMatijasevic] p. 696Theorem 2.18jm2.18 36448
[JonesMatijasevic] p. 697Lemma 2.24jm2.24 36423  jm2.24nn 36419
[JonesMatijasevic] p. 697Lemma 2.26jm2.26 36462
[JonesMatijasevic] p. 697Lemma 2.27jm2.27 36468  rmygeid 36424
[JonesMatijasevic] p. 698Lemma 3.1jm3.1 36480
[Juillerat] p. 11Section *5etransc 39070  etransclem47 39067  etransclem48 39069
[Juillerat] p. 12Equation (7)etransclem44 39064
[Juillerat] p. 12Equation *(7)etransclem46 39066
[Juillerat] p. 12Proof of the derivative calculatedetransclem32 39052
[Juillerat] p. 13Proofetransclem35 39055
[Juillerat] p. 13Part of case 2 proven inetransclem38 39058
[Juillerat] p. 13Part of case 2 provenetransclem24 39044
[Juillerat] p. 13Part of case 2: proven inetransclem41 39061
[Juillerat] p. 14Proofetransclem23 39043
[KalishMontague] p. 81Note 1ax-6 1838
[KalishMontague] p. 85Lemma 2equid 1889
[KalishMontague] p. 85Lemma 3equcomi 1894
[KalishMontague] p. 86Lemma 7cbvalivw 1884  cbvaliw 1883
[KalishMontague] p. 87Lemma 8spimvw 1877  spimw 1876
[KalishMontague] p. 87Lemma 9spfw 1915  spw 1916
[Kalmbach] p. 14Definition of latticechabs1 27548  chabs1i 27550  chabs2 27549  chabs2i 27551  chjass 27565  chjassi 27518  latabs1 16800  latabs2 16801
[Kalmbach] p. 15Definition of atomdf-at 28370  ela 28371
[Kalmbach] p. 15Definition of coverscvbr2 28315  cvrval2 33454
[Kalmbach] p. 16Definitiondf-ol 33358  df-oml 33359
[Kalmbach] p. 20Definition of commutescmbr 27616  cmbri 27622  cmtvalN 33391  df-cm 27615  df-cmtN 33357
[Kalmbach] p. 22Remarkomllaw5N 33427  pjoml5 27645  pjoml5i 27620
[Kalmbach] p. 22Definitionpjoml2 27643  pjoml2i 27617
[Kalmbach] p. 22Theorem 2(v)cmcm 27646  cmcmi 27624  cmcmii 27629  cmtcomN 33429
[Kalmbach] p. 22Theorem 2(ii)omllaw3 33425  omlsi 27436  pjoml 27468  pjomli 27467
[Kalmbach] p. 22Definition of OML lawomllaw2N 33424
[Kalmbach] p. 23Remarkcmbr2i 27628  cmcm3 27647  cmcm3i 27626  cmcm3ii 27631  cmcm4i 27627  cmt3N 33431  cmt4N 33432  cmtbr2N 33433
[Kalmbach] p. 23Lemma 3cmbr3 27640  cmbr3i 27632  cmtbr3N 33434
[Kalmbach] p. 25Theorem 5fh1 27650  fh1i 27653  fh2 27651  fh2i 27654  omlfh1N 33438
[Kalmbach] p. 65Remarkchjatom 28389  chslej 27530  chsleji 27490  shslej 27412  shsleji 27402
[Kalmbach] p. 65Proposition 1chocin 27527  chocini 27486  chsupcl 27372  chsupval2 27442  h0elch 27285  helch 27273  hsupval2 27441  ocin 27328  ococss 27325  shococss 27326
[Kalmbach] p. 65Definition of subspace sumshsval 27344
[Kalmbach] p. 66Remarkdf-pjh 27427  pjssmi 28197  pjssmii 27713
[Kalmbach] p. 67Lemma 3osum 27677  osumi 27674
[Kalmbach] p. 67Lemma 4pjci 28232
[Kalmbach] p. 103Exercise 6atmd2 28432
[Kalmbach] p. 103Exercise 12mdsl0 28342
[Kalmbach] p. 140Remarkhatomic 28392  hatomici 28391  hatomistici 28394
[Kalmbach] p. 140Proposition 1atlatmstc 33499
[Kalmbach] p. 140Proposition 1(i)atexch 28413  lsatexch 33223
[Kalmbach] p. 140Proposition 1(ii)chcv1 28387  cvlcvr1 33519  cvr1 33589
[Kalmbach] p. 140Proposition 1(iii)cvexch 28406  cvexchi 28401  cvrexch 33599
[Kalmbach] p. 149Remark 2chrelati 28396  hlrelat 33581  hlrelat5N 33580  lrelat 33194
[Kalmbach] p. 153Exercise 5lsmcv 18864  lsmsatcv 33190  spansncv 27685  spansncvi 27684
[Kalmbach] p. 153Proposition 1(ii)lsmcv2 33209  spansncv2 28325
[Kalmbach] p. 266Definitiondf-st 28243
[Kalmbach2] p. 8Definition of adjointdf-adjh 27881
[KanamoriPincus] p. 415Theorem 1.1fpwwe 9222  fpwwe2 9219
[KanamoriPincus] p. 416Corollary 1.3canth4 9223
[KanamoriPincus] p. 417Corollary 1.6canthp1 9230
[KanamoriPincus] p. 417Corollary 1.4(a)canthnum 9225
[KanamoriPincus] p. 417Corollary 1.4(b)canthwe 9227
[KanamoriPincus] p. 418Proposition 1.7pwfseq 9240
[KanamoriPincus] p. 419Lemma 2.2gchcdaidm 9244  gchxpidm 9245
[KanamoriPincus] p. 419Theorem 2.1gchacg 9256  gchhar 9255
[KanamoriPincus] p. 420Lemma 2.3pwcdadom 8796  unxpwdom 8252
[KanamoriPincus] p. 421Proposition 3.1gchpwdom 9246
[Kreyszig] p. 3Property M1metcl 21847  xmetcl 21846
[Kreyszig] p. 4Property M2meteq0 21854
[Kreyszig] p. 8Definition 1.1-8dscmet 22087
[Kreyszig] p. 12Equation 5conjmul 10490  muleqadd 10419
[Kreyszig] p. 18Definition 1.3-2mopnval 21953
[Kreyszig] p. 19Remarkmopntopon 21954
[Kreyszig] p. 19Theorem T1mopn0 22013  mopnm 21959
[Kreyszig] p. 19Theorem T2unimopn 22011
[Kreyszig] p. 19Definition of neighborhoodneibl 22016
[Kreyszig] p. 20Definition 1.3-3metcnp2 22057
[Kreyszig] p. 25Definition 1.4-1lmbr 20773  lmmbr 22729  lmmbr2 22730
[Kreyszig] p. 26Lemma 1.4-2(a)lmmo 20895
[Kreyszig] p. 28Theorem 1.4-5lmcau 22783
[Kreyszig] p. 28Definition 1.4-3iscau 22747  iscmet2 22765
[Kreyszig] p. 30Theorem 1.4-7cmetss 22785
[Kreyszig] p. 30Theorem 1.4-6(a)1stcelcls 20975  metelcls 22775
[Kreyszig] p. 30Theorem 1.4-6(b)metcld 22776  metcld2 22777
[Kreyszig] p. 51Equation 2clmvneg1 22623  lmodvneg1 18631  nvinv 26637  vcm 26565
[Kreyszig] p. 51Equation 1aclm0vs 22622  lmod0vs 18624  slmd0vs 28905  vc0 26563
[Kreyszig] p. 51Equation 1blmodvs0 18625  slmdvs0 28906  vcz 26564
[Kreyszig] p. 58Definition 2.2-1imsmet 26700
[Kreyszig] p. 59Equation 1imsdval 26695  imsdval2 26696
[Kreyszig] p. 63Problem 1nvnd 26697
[Kreyszig] p. 64Problem 2nvge0 26680  nvz 26675
[Kreyszig] p. 64Problem 3nvabs 26679
[Kreyszig] p. 91Definition 2.7-1isblo3i 26819
[Kreyszig] p. 92Equation 2df-nmoo 26763
[Kreyszig] p. 97Theorem 2.7-9(a)blocn 26825  blocni 26823
[Kreyszig] p. 97Theorem 2.7-9(b)lnocni 26824
[Kreyszig] p. 129Definition 3.1-1cphipeq0 22682  ipeq0 19706  ipz 26735
[Kreyszig] p. 135Problem 2pythi 26868
[Kreyszig] p. 137Lemma 3-2.1(a)sii 26872
[Kreyszig] p. 144Equation 4supcvg 14294
[Kreyszig] p. 144Theorem 3.3-1minvec 22879  minveco 26903
[Kreyszig] p. 196Definition 3.9-1df-aj 26768
[Kreyszig] p. 247Theorem 4.7-2bcth 22798
[Kreyszig] p. 249Theorem 4.7-3ubth 26892
[Kreyszig] p. 470Definition of positive operator orderingleop 28155  leopg 28154
[Kreyszig] p. 476Theorem 9.4-2opsqrlem2 28173
[Kreyszig] p. 525Theorem 10.1-1htth 26948
[Kulpa] p. 547Theorempoimir 32487
[Kulpa] p. 547Equation (1)poimirlem32 32486
[Kulpa] p. 547Equation (2)poimirlem31 32485
[Kulpa] p. 548Theorembroucube 32488
[Kulpa] p. 548Equation (6)poimirlem26 32480
[Kulpa] p. 548Equation (7)poimirlem27 32481
[Kunen] p. 10Axiom 0ax6e 2141  axnul 4614
[Kunen] p. 11Axiom 3axnul 4614
[Kunen] p. 12Axiom 6zfrep6 6901
[Kunen] p. 24Definition 10.24mapval 7631  mapvalg 7629
[Kunen] p. 30Lemma 10.20fodom 9102
[Kunen] p. 31Definition 10.24mapex 7625
[Kunen] p. 95Definition 2.1df-r1 8385
[Kunen] p. 97Lemma 2.10r1elss 8427  r1elssi 8426
[Kunen] p. 107Exercise 4rankop 8479  rankopb 8473  rankuni 8484  rankxplim 8500  rankxpsuc 8503
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 4365
[Lang] p. 3Definitiondf-mnd 17008
[Lang] p. 7Definitiondfgrp2e 17161
[Lang] p. 53Definitiondf-cat 16042
[Lang] p. 54Definitiondf-iso 16122
[Lang] p. 57Definitiondf-inito 16354  df-termo 16355
[Lang] p. 58Exampleirinitoringc 41953
[Lang] p. 58Statementinitoeu1 16374  termoeu1 16381
[Lang] p. 62Definitiondf-func 16231
[Lang] p. 65Definitiondf-nat 16316
[Lang] p. 91Notedf-ringc 41889
[Lang] p. 128Remarkdsmmlmod 19809
[Lang] p. 129Prooflincscm 42105  lincscmcl 42107  lincsum 42104  lincsumcl 42106
[Lang] p. 129Statementlincolss 42109
[Lang] p. 129Observationdsmmfi 19802
[Lang] p. 147Definitionsnlindsntor 42146
[Lang] p. 504Statementmat1 19973  matring 19969
[Lang] p. 504Definitiondf-mamu 19910
[Lang] p. 505Statementmamuass 19928  mamutpos 19984  matassa 19970  mattposvs 19981  tposmap 19983
[Lang] p. 513Definitionmdet1 20127  mdetf 20121
[Lang] p. 513Theorem 4.4cramer 20217
[Lang] p. 514Proposition 4.6mdetleib 20113
[Lang] p. 514Proposition 4.8mdettpos 20137
[Lang] p. 515Definitiondf-minmar1 20161  smadiadetr 20201
[Lang] p. 515Corollary 4.9mdetero 20136  mdetralt 20134
[Lang] p. 517Proposition 4.15mdetmul 20149
[Lang] p. 518Definitiondf-madu 20160
[Lang] p. 518Proposition 4.16madulid 20171  madurid 20170  matinv 20203
[Lang] p. 561Theorem 3.1cayleyhamilton 20415
[Lang], p. 561Remarkchpmatply1 20357
[Lang], p. 561Definitiondf-chpmat 20352
[LarsonHostetlerEdwards] p. 278Section 4.1dvconstbi 37437
[LarsonHostetlerEdwards] p. 311Example 1alhe4.4ex1a 37432
[LarsonHostetlerEdwards] p. 375Theorem 5.1expgrowth 37438
[LeBlanc] p. 277Rule R2axnul 4614
[Levy] p. 338Axiomdf-clab 2501  df-clel 2510  df-cleq 2507
[Levy58] p. 2Definition Iisfin1-3 8966
[Levy58] p. 2Definition IIdf-fin2 8866
[Levy58] p. 2Definition Iadf-fin1a 8865
[Levy58] p. 2Definition IIIdf-fin3 8868
[Levy58] p. 3Definition Vdf-fin5 8869
[Levy58] p. 3Definition IVdf-fin4 8867
[Levy58] p. 4Definition VIdf-fin6 8870
[Levy58] p. 4Definition VIIdf-fin7 8871
[Levy58], p. 3Theorem 1fin1a2 8995
[Lopez-Astorga] p. 12Rule 1mptnan 1683
[Lopez-Astorga] p. 12Rule 2mptxor 1684
[Lopez-Astorga] p. 12Rule 3mtpxor 1686
[Maeda] p. 167Theorem 1(d) to (e)mdsymlem6 28440
[Maeda] p. 168Lemma 5mdsym 28444  mdsymi 28443
[Maeda] p. 168Lemma 4(i)mdsymlem4 28438  mdsymlem6 28440  mdsymlem7 28441
[Maeda] p. 168Lemma 4(ii)mdsymlem8 28442
[MaedaMaeda] p. 1Remarkssdmd1 28345  ssdmd2 28346  ssmd1 28343  ssmd2 28344
[MaedaMaeda] p. 1Lemma 1.2mddmd2 28341
[MaedaMaeda] p. 1Definition 1.1df-dmd 28313  df-md 28312  mdbr 28326
[MaedaMaeda] p. 2Lemma 1.3mdsldmd1i 28363  mdslj1i 28351  mdslj2i 28352  mdslle1i 28349  mdslle2i 28350  mdslmd1i 28361  mdslmd2i 28362
[MaedaMaeda] p. 2Lemma 1.4mdsl1i 28353  mdsl2bi 28355  mdsl2i 28354
[MaedaMaeda] p. 2Lemma 1.6mdexchi 28367
[MaedaMaeda] p. 2Lemma 1.5.1mdslmd3i 28364
[MaedaMaeda] p. 2Lemma 1.5.2mdslmd4i 28365
[MaedaMaeda] p. 2Lemma 1.5.3mdsl0 28342
[MaedaMaeda] p. 2Theorem 1.3dmdsl3 28347  mdsl3 28348
[MaedaMaeda] p. 3Theorem 1.9.1csmdsymi 28366
[MaedaMaeda] p. 4Theorem 1.14mdcompli 28461
[MaedaMaeda] p. 30Lemma 7.2atlrelat1 33501  hlrelat1 33579
[MaedaMaeda] p. 31Lemma 7.5lcvexch 33219
[MaedaMaeda] p. 31Lemma 7.5.1cvmd 28368  cvmdi 28356  cvnbtwn4 28321  cvrnbtwn4 33459
[MaedaMaeda] p. 31Lemma 7.5.2cvdmd 28369
[MaedaMaeda] p. 31Definition 7.4cvlcvrp 33520  cvp 28407  cvrp 33595  lcvp 33220
[MaedaMaeda] p. 31Theorem 7.6(b)atmd 28431
[MaedaMaeda] p. 31Theorem 7.6(c)atdmd 28430
[MaedaMaeda] p. 32Definition 7.8cvlexch4N 33513  hlexch4N 33571
[MaedaMaeda] p. 34Exercise 7.1atabsi 28433
[MaedaMaeda] p. 41Lemma 9.2(delta)cvrat4 33622
[MaedaMaeda] p. 61Definition 15.10psubN 33928  atpsubN 33932  df-pointsN 33681  pointpsubN 33930
[MaedaMaeda] p. 62Theorem 15.5df-pmap 33683  pmap11 33941  pmaple 33940  pmapsub 33947  pmapval 33936
[MaedaMaeda] p. 62Theorem 15.5.1pmap0 33944  pmap1N 33946
[MaedaMaeda] p. 62Theorem 15.5.2pmapglb 33949  pmapglb2N 33950  pmapglb2xN 33951  pmapglbx 33948
[MaedaMaeda] p. 63Equation 15.5.3pmapjoin 34031
[MaedaMaeda] p. 67Postulate PS1ps-1 33656
[MaedaMaeda] p. 68Lemma 16.2df-padd 33975  paddclN 34021  paddidm 34020
[MaedaMaeda] p. 68Condition PS2ps-2 33657
[MaedaMaeda] p. 68Equation 16.2.1paddass 34017
[MaedaMaeda] p. 69Lemma 16.4ps-1 33656
[MaedaMaeda] p. 69Theorem 16.4ps-2 33657
[MaedaMaeda] p. 70Theorem 16.9lsmmod 17817  lsmmod2 17818  lssats 33192  shatomici 28390  shatomistici 28393  shmodi 27422  shmodsi 27421
[MaedaMaeda] p. 130Remark 29.6dmdmd 28332  mdsymlem7 28441
[MaedaMaeda] p. 132Theorem 29.13(e)pjoml6i 27621
[MaedaMaeda] p. 136Lemma 31.1.5shjshseli 27525
[MaedaMaeda] p. 139Remarksumdmdii 28447
[Margaris] p. 40Rule Cexlimiv 1811
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[Margaris] p. 49Definitiondf-an 384  df-ex 1695  df-or 383  dfbi2 657
[Margaris] p. 51Theorem 1idALT 23
[Margaris] p. 56Theorem 3conventions 26389
[Margaris] p. 59Section 14notnotrALTVD 38055
[Margaris] p. 60Theorem 8mth8 156
[Margaris] p. 60Section 14con3ALTVD 38056
[Margaris] p. 79Rule Cexinst01 37753  exinst11 37754
[Margaris] p. 89Theorem 19.219.2 1842  19.2g 1999  r19.2z 3915
[Margaris] p. 89Theorem 19.319.3 2018  rr19.3v 3218
[Margaris] p. 89Theorem 19.5alcom 1974
[Margaris] p. 89Theorem 19.6alex 1731
[Margaris] p. 89Theorem 19.7alnex 1696
[Margaris] p. 89Theorem 19.819.8a 1988
[Margaris] p. 89Theorem 19.919.9 2022  19.9h 2023  exlimd 2045  exlimdh 2046
[Margaris] p. 89Theorem 19.11excom 1978  excomim 1979
[Margaris] p. 89Theorem 19.1219.12 2082
[Margaris] p. 90Section 19conventions-label 26390  conventions-label 26390  conventions-label 26390  conventions-label 26390
[Margaris] p. 90Theorem 19.14exnal 1732
[Margaris] p. 90Theorem 19.152albi 37481  albi 1721
[Margaris] p. 90Theorem 19.1619.16 2087
[Margaris] p. 90Theorem 19.1719.17 2088
[Margaris] p. 90Theorem 19.182exbi 37483  exbi 1750
[Margaris] p. 90Theorem 19.1919.19 2089
[Margaris] p. 90Theorem 19.202alim 37480  2alimdv 1800  alimd 2007  alimdh 1720  alimdv 1798  ax-4 1713  ralimdaa 2845  ralimdv 2850  ralimdva 2849  ralimdvva 2851  sbcimdv 3369
[Margaris] p. 90Theorem 19.2119.21 2036  19.21h 2038  19.21t 2035  19.21vv 37479  alrimd 2012  alrimdd 2011  alrimdh 1758  alrimdv 1810  alrimi 2008  alrimih 1726  alrimiv 1808  alrimivv 1809  hbralrimi 2841  r19.21be 2821  r19.21bi 2820  ralrimd 2846  ralrimdv 2855  ralrimdva 2856  ralrimdvv 2860  ralrimdvva 2861  ralrimi 2844  ralrimiv 2852  ralrimiva 2853  ralrimivv 2857  ralrimivva 2858  ralrimivvva 2859  ralrimivw 2854  wl-19.21 32327  wl-19.21t 32326  wl-alrimi 32330
[Margaris] p. 90Theorem 19.222exim 37482  2eximdv 1801  exim 1739  eximd 2013  eximdh 1759  eximdv 1799  rexim 2895  reximd2a 2900  reximdai 2899  reximddv 2905  reximddv2 2906  reximdv 2903  reximdv2 2901  reximdva 2904  reximdvai 2902  reximi2 2897
[Margaris] p. 90Theorem 19.2319.23 2041  19.23bi 2002  19.23h 2042  19.23t 2040  exlimdv 1814  exlimdvv 1815  exlimexi 37633  exlimiv 1811  exlimivv 1813  rexlimdv 2916  rexlimdv3a 2919  rexlimdva 2917  rexlimdvaa 2918  rexlimdvv 2923  rexlimdvva 2924  rexlimdvw 2920  rexlimiv 2913  rexlimiva 2914  rexlimivv 2922  wl-19.23 32329
[Margaris] p. 90Theorem 19.2419.24 1850
[Margaris] p. 90Theorem 19.2519.25 1778
[Margaris] p. 90Theorem 19.2619.26 1767
[Margaris] p. 90Theorem 19.2719.27 2054  r19.27z 3925  r19.27zv 3926
[Margaris] p. 90Theorem 19.2819.28 2055  19.28vv 37489  r19.28z 3918  r19.28zv 3921  rr19.28v 3219
[Margaris] p. 90Theorem 19.2919.29 1770  r19.29d2r 2965  r19.29imd 2960
[Margaris] p. 90Theorem 19.3019.30 1779
[Margaris] p. 90Theorem 19.3119.31 2097  19.31vv 37487
[Margaris] p. 90Theorem 19.3219.32 2096  r19.32 39710
[Margaris] p. 90Theorem 19.3319.33-2 37485  19.33 1782
[Margaris] p. 90Theorem 19.3419.34 1851
[Margaris] p. 90Theorem 19.3519.35 1775
[Margaris] p. 90Theorem 19.3619.36 2093  19.36vv 37486  r19.36zv 3927
[Margaris] p. 90Theorem 19.3719.37 2095  19.37vv 37488  r19.37zv 3922
[Margaris] p. 90Theorem 19.3819.38 1745
[Margaris] p. 90Theorem 19.3919.39 1849
[Margaris] p. 90Theorem 19.4019.40-2 1784  19.40 1766  r19.40 2973
[Margaris] p. 90Theorem 19.4119.41 2101  19.41rg 37669
[Margaris] p. 90Theorem 19.4219.42 2103
[Margaris] p. 90Theorem 19.4319.43 1780
[Margaris] p. 90Theorem 19.4419.44 2098  r19.44zv 3924
[Margaris] p. 90Theorem 19.4519.45 2099  r19.45zv 3923
[Margaris] p. 90Theorem 1977.23wl-19.23t 32328
[Margaris] p. 110Exercise 2(b)eu1 2402
[Mayet] p. 370Remarkjpi 28302  largei 28299  stri 28289
[Mayet3] p. 9Definition of CH-statesdf-hst 28244  ishst 28246
[Mayet3] p. 10Theoremhstrbi 28298  hstri 28297
[Mayet3] p. 1223Theorem 4.1mayete3i 27760
[Mayet3] p. 1240Theorem 7.1mayetes3i 27761
[MegPav2000] p. 2344Theorem 3.3stcltrthi 28310
[MegPav2000] p. 2345Definition 3.4-1chintcl 27364  chsupcl 27372
[MegPav2000] p. 2345Definition 3.4-2hatomic 28392
[MegPav2000] p. 2345Definition 3.4-3(a)superpos 28386
[MegPav2000] p. 2345Definition 3.4-3(b)atexch 28413
[MegPav2000] p. 2366Figure 7pl42N 34162
[MegPav2002] p. 362Lemma 2.2latj31 16812  latj32 16810  latjass 16808
[Megill] p. 444Axiom C5ax-5 1793  ax5ALT 33085
[Megill] p. 444Section 7conventions 26389
[Megill] p. 445Lemma L12aecom-o 33079  ax-c11n 33066  axc11n 2199
[Megill] p. 446Lemma L17equtrr 1899
[Megill] p. 446Lemma L18ax6fromc10 33074
[Megill] p. 446Lemma L19hbnae-o 33106  hbnae 2209
[Megill] p. 447Remark 9.1df-sb 1831  sbid 2133  sbidd-misc 42312  sbidd 42311
[Megill] p. 448Remark 9.6axc14 2264
[Megill] p. 448Scheme C4'ax-c4 33062
[Megill] p. 448Scheme C5'ax-c5 33061  sp 1990
[Megill] p. 448Scheme C6'ax-11 1971
[Megill] p. 448Scheme C7'ax-c7 33063
[Megill] p. 448Scheme C8'ax-7 1885
[Megill] p. 448Scheme C9'ax-c9 33068
[Megill] p. 448Scheme C10'ax-6 1838  ax-c10 33064
[Megill] p. 448Scheme C11'ax-c11 33065
[Megill] p. 448Scheme C12'ax-8 1940
[Megill] p. 448Scheme C13'ax-9 1947
[Megill] p. 448Scheme C14'ax-c14 33069
[Megill] p. 448Scheme C15'ax-c15 33067
[Megill] p. 448Scheme C16'ax-c16 33070
[Megill] p. 448Theorem 9.4dral1-o 33082  dral1 2217  dral2-o 33108  dral2 2216  drex1 2219  drex2 2220  drsb1 2269  drsb2 2270
[Megill] p. 449Theorem 9.7sbcom2 2337  sbequ 2268  sbid2v 2349
[Megill] p. 450Example in Appendixhba1-o 33075  hba1 2026
[Mendelson] p. 35Axiom A3hirstL-ax3 39602
[Mendelson] p. 36Lemma 1.8idALT 23
[Mendelson] p. 69Axiom 4rspsbc 3388  rspsbca 3389  stdpc4 2245
[Mendelson] p. 69Axiom 5ax-c4 33062  ra4 3395  stdpc5 2039
[Mendelson] p. 81Rule Cexlimiv 1811
[Mendelson] p. 95Axiom 6stdpc6 1907
[Mendelson] p. 95Axiom 7stdpc7 1908
[Mendelson] p. 225Axiom system NBGru 3305
[Mendelson] p. 230Exercise 4.8(b)opthwiener 4796
[Mendelson] p. 231Exercise 4.10(k)inv1 3825
[Mendelson] p. 231Exercise 4.10(l)unv 3826
[Mendelson] p. 231Exercise 4.10(n)dfin3 3728
[Mendelson] p. 231Exercise 4.10(o)df-nul 3778
[Mendelson] p. 231Exercise 4.10(q)dfin4 3729
[Mendelson] p. 231Exercise 4.10(s)ddif 3608
[Mendelson] p. 231Definition of uniondfun3 3727
[Mendelson] p. 235Exercise 4.12(c)univ 4744
[Mendelson] p. 235Exercise 4.12(d)pwv 4269
[Mendelson] p. 235Exercise 4.12(j)pwin 4836
[Mendelson] p. 235Exercise 4.12(k)pwunss 4837
[Mendelson] p. 235Exercise 4.12(l)pwssun 4838
[Mendelson] p. 235Exercise 4.12(n)uniin 4291
[Mendelson] p. 235Exercise 4.12(p)reli 5063
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5463
[Mendelson] p. 244Proposition 4.8(g)epweon 6750
[Mendelson] p. 246Definition of successordf-suc 5536
[Mendelson] p. 250Exercise 4.36oelim2 7437
[Mendelson] p. 254Proposition 4.22(b)xpen 7883
[Mendelson] p. 254Proposition 4.22(c)xpsnen 7804  xpsneng 7805
[Mendelson] p. 254Proposition 4.22(d)xpcomen 7811  xpcomeng 7812
[Mendelson] p. 254Proposition 4.22(e)xpassen 7814
[Mendelson] p. 255Definitionbrsdom 7739
[Mendelson] p. 255Exercise 4.39endisj 7807
[Mendelson] p. 255Exercise 4.41mapprc 7623
[Mendelson] p. 255Exercise 4.43mapsnen 7795
[Mendelson] p. 255Exercise 4.45mapunen 7889
[Mendelson] p. 255Exercise 4.47xpmapen 7888
[Mendelson] p. 255Exercise 4.42(a)map0e 7656
[Mendelson] p. 255Exercise 4.42(b)map1 7796
[Mendelson] p. 257Proposition 4.24(a)undom 7808
[Mendelson] p. 258Exercise 4.56(b)cdaen 8753
[Mendelson] p. 258Exercise 4.56(c)cdaassen 8762  cdacomen 8761
[Mendelson] p. 258Exercise 4.56(f)cdadom1 8766
[Mendelson] p. 258Exercise 4.56(g)xp2cda 8760
[Mendelson] p. 258Definition of cardinal sumcdaval 8750  df-cda 8748
[Mendelson] p. 266Proposition 4.34(a)oa1suc 7373
[Mendelson] p. 266Proposition 4.34(f)oaordex 7400
[Mendelson] p. 275Proposition 4.42(d)entri3 9135
[Mendelson] p. 281Definitiondf-r1 8385
[Mendelson] p. 281Proposition 4.45 (b) to (a)unir1 8434
[Mendelson] p. 287Axiom system MKru 3305
[MertziosUnger] p. 152Definitiondf-frgr 41521
[MertziosUnger] p. 153Remark 1frconngra 26287  frgrconngr 41556
[MertziosUnger] p. 153Remark 2vdgn1frgrav2 26292  vdgn1frgrav3 26294  vdgn1frgrv2 41558  vdgn1frgrv3 41559  vdn1frgrav2 26291
[MertziosUnger] p. 153Remark 3vdgfrgragt2 26293  vdgfrgrgt2 41560
[MertziosUnger] p. 153Proposition 1(a)n4cyclfrgr 41553  n4cyclfrgra 26284
[MertziosUnger] p. 153Proposition 1(b)2pthfrgr 41546  2pthfrgra 26277  2pthfrgrarn 26275  2pthfrgrarn2 26276  2pthfrgrrn 41544  2pthfrgrrn2 41545
[Mittelstaedt] p. 9Definitiondf-oc 27282
[Monk1] p. 22Remarkconventions 26389
[Monk1] p. 22Theorem 3.1conventions 26389
[Monk1] p. 26Theorem 2.8(vii)ssin 3700
[Monk1] p. 33Theorem 3.2(i)ssrel 5024  ssrelf 28594
[Monk1] p. 33Theorem 3.2(ii)eqrel 5025
[Monk1] p. 34Definition 3.3df-opab 4542
[Monk1] p. 36Theorem 3.7(i)coi1 5458  coi2 5459
[Monk1] p. 36Theorem 3.8(v)dm0 5151  rn0 5189
[Monk1] p. 36Theorem 3.7(ii)cnvi 5346
[Monk1] p. 37Theorem 3.13(i)relxp 5043
[Monk1] p. 37Theorem 3.13(x)dmxp 5156  rnxp 5373
[Monk1] p. 37Theorem 3.13(ii)0xp 5016  xp0 5361
[Monk1] p. 38Theorem 3.16(ii)ima0 5290
[Monk1] p. 38Theorem 3.16(viii)imai 5287
[Monk1] p. 39Theorem 3.17imaexg 6870
[Monk1] p. 39Theorem 3.16(xi)imassrn 5286
[Monk1] p. 41Theorem 4.3(i)fnopfv 6142  funfvop 6120
[Monk1] p. 42Theorem 4.3(ii)funopfvb 6032
[Monk1] p. 42Theorem 4.4(iii)fvelima 6041
[Monk1] p. 43Theorem 4.6funun 5731
[Monk1] p. 43Theorem 4.8(iv)dff13 6292  dff13f 6293
[Monk1] p. 46Theorem 4.15(v)funex 6263  funrnex 6900
[Monk1] p. 50Definition 5.4fniunfv 6285
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5427
[Monk1] p. 52Theorem 5.11(viii)ssint 4326
[Monk1] p. 52Definition 5.13 (i)1stval2 6950  df-1st 6933
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6951  df-2nd 6934
[Monk1] p. 112Theorem 15.17(v)ranksn 8475  ranksnb 8448
[Monk1] p. 112Theorem 15.17(iv)rankuni2 8476
[Monk1] p. 112Theorem 15.17(iii)rankun 8477  rankunb 8471
[Monk1] p. 113Theorem 15.18r1val3 8459
[Monk1] p. 113Definition 15.19df-r1 8385  r1val2 8458
[Monk1] p. 117Lemmazorn2 9086  zorn2g 9083
[Monk1] p. 133Theorem 18.11cardom 8570
[Monk1] p. 133Theorem 18.12canth3 9137
[Monk1] p. 133Theorem 18.14carduni 8565
[Monk2] p. 105Axiom C4ax-4 1713
[Monk2] p. 105Axiom C7ax-7 1885
[Monk2] p. 105Axiom C8ax-12 1983  ax-c15 33067  ax12v2 1985
[Monk2] p. 108Lemma 5ax-c4 33062
[Monk2] p. 109Lemma 12ax-11 1971
[Monk2] p. 109Lemma 15equvini 2238  equvinv 1909  eqvinop 4779
[Monk2] p. 113Axiom C5-1ax-5 1793  ax5ALT 33085
[Monk2] p. 113Axiom C5-2ax-10 1966
[Monk2] p. 113Axiom C5-3ax-11 1971
[Monk2] p. 114Lemma 21sp 1990
[Monk2] p. 114Lemma 22axc4 1991  hba1-o 33075  hba1 2026
[Monk2] p. 114Lemma 23nfia1 2086
[Monk2] p. 114Lemma 24nfa2 2085  nfra2 2834
[Moore] p. 53Part Idf-mre 15959
[Munkres] p. 77Example 2distop 20511  indistop 20517  indistopon 20516
[Munkres] p. 77Example 3fctop 20519  fctop2 20520
[Munkres] p. 77Example 4cctop 20521
[Munkres] p. 78Definition of basisdf-bases 20423  isbasis3g 20465
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 15809  tgval2 20472
[Munkres] p. 79Remarktgcl 20485
[Munkres] p. 80Lemma 2.1tgval3 20479
[Munkres] p. 80Lemma 2.2tgss2 20503  tgss3 20502
[Munkres] p. 81Lemma 2.3basgen 20504  basgen2 20505
[Munkres] p. 83Exercise 3topdifinf 32205  topdifinfeq 32206  topdifinffin 32204  topdifinfindis 32202
[Munkres] p. 89Definition of subspace topologyresttop 20675
[Munkres] p. 93Theorem 6.1(1)0cld 20553  topcld 20550
[Munkres] p. 93Theorem 6.1(2)iincld 20554
[Munkres] p. 93Theorem 6.1(3)uncld 20556
[Munkres] p. 94Definition of closureclsval 20552
[Munkres] p. 94Definition of interiorntrval 20551
[Munkres] p. 95Theorem 6.5(a)clsndisj 20590  elcls 20588
[Munkres] p. 95Theorem 6.5(b)elcls3 20598
[Munkres] p. 97Theorem 6.6clslp 20663  neindisj 20632
[Munkres] p. 97Corollary 6.7cldlp 20665
[Munkres] p. 97Definition of limit pointislp2 20660  lpval 20654
[Munkres] p. 98Definition of Hausdorff spacedf-haus 20830
[Munkres] p. 102Definition of continuous functiondf-cn 20742  iscn 20750  iscn2 20753
[Munkres] p. 107Theorem 7.2(g)cncnp 20795  cncnp2 20796  cncnpi 20793  df-cnp 20743  iscnp 20752  iscnp2 20754
[Munkres] p. 127Theorem 10.1metcn 22058
[Munkres] p. 128Theorem 10.3metcn4 22781
[NielsenChuang] p. 195Equation 4.73unierri 28136
[OeSilva] p. Resultax-bgbltosilva 40121
[Pfenning] p. 17Definition XMnatded 26391
[Pfenning] p. 17Definition NNCnatded 26391  notnotrd 126
[Pfenning] p. 17Definition ` `Cnatded 26391
[Pfenning] p. 18Rule"natded 26391
[Pfenning] p. 18Definition /\Inatded 26391
[Pfenning] p. 18Definition ` `Enatded 26391  natded 26391  natded 26391  natded 26391  natded 26391
[Pfenning] p. 18Definition ` `Inatded 26391  natded 26391  natded 26391  natded 26391  natded 26391
[Pfenning] p. 18Definition ` `ELnatded 26391
[Pfenning] p. 18Definition ` `ERnatded 26391
[Pfenning] p. 18Definition ` `Ea,unatded 26391
[Pfenning] p. 18Definition ` `IRnatded 26391
[Pfenning] p. 18Definition ` `Ianatded 26391
[Pfenning] p. 127Definition =Enatded 26391
[Pfenning] p. 127Definition =Inatded 26391
[Ponnusamy] p. 361Theorem 6.44cphip0l 22680  df-dip 26714  dip0l 26734  ip0l 19704
[Ponnusamy] p. 361Equation 6.45ipval 26716
[Ponnusamy] p. 362Equation I1dipcj 26730
[Ponnusamy] p. 362Equation I3cphdir 22683  dipdir 26860  ipdir 19707  ipdiri 26848
[Ponnusamy] p. 362Equation I4ipidsq 26726
[Ponnusamy] p. 362Equation 6.46ip0i 26843
[Ponnusamy] p. 362Equation 6.47ip1i 26845
[Ponnusamy] p. 362Equation 6.48ip2i 26846
[Ponnusamy] p. 363Equation I2cphass 22689  dipass 26863  ipass 19713  ipassi 26859
[Prugovecki] p. 186Definition of brabraval 27976  df-bra 27882
[Prugovecki] p. 376Equation 8.1df-kb 27883  kbval 27986
[PtakPulmannova] p. 66Proposition 3.2.17atomli 28414
[PtakPulmannova] p. 68Lemma 3.1.4df-pclN 34067
[PtakPulmannova] p. 68Lemma 3.2.20atcvat3i 28428  atcvat4i 28429  cvrat3 33621  cvrat4 33622  lsatcvat3 33232
[PtakPulmannova] p. 68Definition 3.2.18cvbr 28314  cvrval 33449  df-cv 28311  df-lcv 33199  lspsncv0 18869
[PtakPulmannova] p. 72Lemma 3.3.6pclfinN 34079
[PtakPulmannova] p. 74Lemma 3.3.10pclcmpatN 34080
[Quine] p. 16Definition 2.1df-clab 2501  rabid 2999
[Quine] p. 17Definition 2.1''dfsb7 2347
[Quine] p. 18Definition 2.7df-cleq 2507
[Quine] p. 19Definition 2.9conventions 26389  df-v 3079
[Quine] p. 34Theorem 5.1abeq2 2623
[Quine] p. 35Theorem 5.2abid1 2635  abid2f 2681
[Quine] p. 40Theorem 6.1sb5 2322
[Quine] p. 40Theorem 6.2sb56 2128  sb6 2321
[Quine] p. 41Theorem 6.3df-clel 2510
[Quine] p. 41Theorem 6.4eqid 2514  eqid1 26454
[Quine] p. 41Theorem 6.5eqcom 2521
[Quine] p. 42Theorem 6.6df-sbc 3307
[Quine] p. 42Theorem 6.7dfsbcq 3308  dfsbcq2 3309
[Quine] p. 43Theorem 6.8vex 3080
[Quine] p. 43Theorem 6.9isset 3084
[Quine] p. 44Theorem 7.3spcgf 3165  spcgv 3170  spcimgf 3163
[Quine] p. 44Theorem 6.11spsbc 3319  spsbcd 3320
[Quine] p. 44Theorem 6.12elex 3089
[Quine] p. 44Theorem 6.13elab 3223  elabg 3224  elabgf 3221
[Quine] p. 44Theorem 6.14noel 3781
[Quine] p. 48Theorem 7.2snprc 4100
[Quine] p. 48Definition 7.1df-pr 4031  df-sn 4029
[Quine] p. 49Theorem 7.4snss 4162  snssg 4171
[Quine] p. 49Theorem 7.5prss 4194  prssg 4193
[Quine] p. 49Theorem 7.6prid1 4144  prid1g 4142  prid2 4145  prid2g 4143  snid 4058  snidg 4056
[Quine] p. 51Theorem 7.12snex 4734
[Quine] p. 51Theorem 7.13prex 4735
[Quine] p. 53Theorem 8.2unisn 4285  unisnALT 38066  unisng 4286
[Quine] p. 53Theorem 8.3uniun 4290
[Quine] p. 54Theorem 8.6elssuni 4301
[Quine] p. 54Theorem 8.7uni0 4299
[Quine] p. 56Theorem 8.17uniabio 5663
[Quine] p. 56Definition 8.18dfiota2 5654
[Quine] p. 57Theorem 8.19iotaval 5664
[Quine] p. 57Theorem 8.22iotanul 5668
[Quine] p. 58Theorem 8.23iotaex 5670
[Quine] p. 58Definition 9.1df-op 4035
[Quine] p. 61Theorem 9.5opabid 4801  opelopab 4816  opelopaba 4810  opelopabaf 4818  opelopabf 4819  opelopabg 4812  opelopabga 4807  opelopabgf 4814  oprabid 6452
[Quine] p. 64Definition 9.11df-xp 4938
[Quine] p. 64Definition 9.12df-cnv 4940
[Quine] p. 64Definition 9.15df-id 4847
[Quine] p. 65Theorem 10.3fun0 5753
[Quine] p. 65Theorem 10.4funi 5719
[Quine] p. 65Theorem 10.5funsn 5738  funsng 5736
[Quine] p. 65Definition 10.1df-fun 5691
[Quine] p. 65Definition 10.2args 5303  dffv4 5983
[Quine] p. 68Definition 10.11conventions 26389  df-fv 5697  fv2 5981
[Quine] p. 124Theorem 17.3nn0opth2 12788  nn0opth2i 12787  nn0opthi 12786  omopthi 7499
[Quine] p. 177Definition 25.2df-rdg 7268
[Quine] p. 232Equation icarddom 9130
[Quine] p. 284Axiom 39(vi)funimaex 5775  funimaexg 5774
[Quine] p. 331Axiom system NFru 3305
[ReedSimon] p. 36Definition (iii)ax-his3 27114
[ReedSimon] p. 63Exercise 4(a)df-dip 26714  polid 27189  polid2i 27187  polidi 27188
[ReedSimon] p. 63Exercise 4(b)df-ph 26831
[ReedSimon] p. 195Remarklnophm 28051  lnophmi 28050
[Retherford] p. 49Exercise 1(i)leopadd 28164
[Retherford] p. 49Exercise 1(ii)leopmul 28166  leopmuli 28165
[Retherford] p. 49Exercise 1(iv)leoptr 28169
[Retherford] p. 49Definition VI.1df-leop 27884  leoppos 28158
[Retherford] p. 49Exercise 1(iii)leoptri 28168
[Retherford] p. 49Definition of operator orderingleop3 28157
[Roman] p. 4Definitiondf-dmat 20016  df-dmatalt 42073
[Roman] p. 18Part Preliminariesdf-rng0 41757
[Roman] p. 19Part Preliminariesdf-ring 18277
[Roman] p. 46Theorem 1.6isldepslvec2 42160
[Roman] p. 112Noteisldepslvec2 42160  ldepsnlinc 42183  zlmodzxznm 42172
[Roman] p. 112Examplezlmodzxzequa 42171  zlmodzxzequap 42174  zlmodzxzldep 42179
[Roman] p. 170Theorem 7.8cayleyhamilton 20415
[Rosenlicht] p. 80Theoremheicant 32489
[Rosser] p. 281Definitiondf-op 4035
[Rotman] p. 28Remarkpgrpgt2nabl 42033  pmtr3ncom 17608
[Rotman] p. 31Theorem 3.4symggen2 17604
[Rotman] p. 42Theorem 3.15cayley 17547  cayleyth 17548
[Rudin] p. 164Equation 27efcan 14532
[Rudin] p. 164Equation 30efzval 14538
[Rudin] p. 167Equation 48absefi 14632
[Sanford] p. 39Remarkax-mp 5  mto 186
[Sanford] p. 39Rule 3mtpxor 1686
[Sanford] p. 39Rule 4mptxor 1684
[Sanford] p. 40Rule 1mptnan 1683
[Schechter] p. 51Definition of antisymmetryintasym 5321
[Schechter] p. 51Definition of irreflexivityintirr 5324
[Schechter] p. 51Definition of symmetrycnvsym 5320
[Schechter] p. 51Definition of transitivitycotr 5318
[Schechter] p. 78Definition of Moore collection of setsdf-mre 15959
[Schechter] p. 79Definition of Moore closuredf-mrc 15960
[Schechter] p. 82Section 4.5df-mrc 15960
[Schechter] p. 84Definition (A) of an algebraic closure systemdf-acs 15962
[Schechter] p. 139Definition AC3dfac9 8716
[Schechter] p. 141Definition (MC)dfac11 36525
[Schechter] p. 149Axiom DC1ax-dc 9026  axdc3 9034
[Schechter] p. 187Definition of ring with unitisring 18279  isrngo 32741
[Schechter] p. 276Remark 11.6.espan0 27574
[Schechter] p. 276Definition of spandf-span 27341  spanval 27365
[Schechter] p. 428Definition 15.35bastop1 20509
[Schwabhauser] p. 10Axiom A1axcgrrflx 25485  axtgcgrrflx 25051
[Schwabhauser] p. 10Axiom A2axcgrtr 25486
[Schwabhauser] p. 10Axiom A3axcgrid 25487  axtgcgrid 25052
[Schwabhauser] p. 10Axioms A1 to A3df-trkgc 25037
[Schwabhauser] p. 11Axiom A4axsegcon 25498  axtgsegcon 25053  df-trkgcb 25039
[Schwabhauser] p. 11Axiom A5ax5seg 25509  axtg5seg 25054  df-trkgcb 25039
[Schwabhauser] p. 11Axiom A6axbtwnid 25510  axtgbtwnid 25055  df-trkgb 25038
[Schwabhauser] p. 12Axiom A7axpasch 25512  axtgpasch 25056  df-trkgb 25038
[Schwabhauser] p. 12Axiom A8axlowdim2 25531  df-trkg2d 29842
[Schwabhauser] p. 13Axiom A8axtglowdim2 25059
[Schwabhauser] p. 13Axiom A9axtgupdim2 25060  df-trkg2d 29842
[Schwabhauser] p. 13Axiom A10axeuclid 25534  axtgeucl 25061  df-trkge 25040
[Schwabhauser] p. 13Axiom A11axcont 25547  axtgcont 25058  axtgcont1 25057  df-trkgb 25038
[Schwabhauser] p. 27Theorem 2.1cgrrflx 31100
[Schwabhauser] p. 27Theorem 2.2cgrcomim 31102
[Schwabhauser] p. 27Theorem 2.3cgrtr 31105
[Schwabhauser] p. 27Theorem 2.4cgrcoml 31109
[Schwabhauser] p. 27Theorem 2.5cgrcomr 31110  tgcgrcomimp 25062  tgcgrcoml 25064  tgcgrcomr 25063
[Schwabhauser] p. 28Theorem 2.8cgrtriv 31115  tgcgrtriv 25069
[Schwabhauser] p. 28Theorem 2.105segofs 31119  tg5segofs 29850
[Schwabhauser] p. 28Definition 2.10df-afs 29847  df-ofs 31096
[Schwabhauser] p. 29Theorem 2.11cgrextend 31121  tgcgrextend 25070
[Schwabhauser] p. 29Theorem 2.12segconeq 31123  tgsegconeq 25071
[Schwabhauser] p. 30Theorem 3.1btwnouttr2 31135  btwntriv2 31125  tgbtwntriv2 25072
[Schwabhauser] p. 30Theorem 3.2btwncomim 31126  tgbtwncom 25073
[Schwabhauser] p. 30Theorem 3.3btwntriv1 31129  tgbtwntriv1 25076
[Schwabhauser] p. 30Theorem 3.4btwnswapid 31130  tgbtwnswapid 25077
[Schwabhauser] p. 30Theorem 3.5btwnexch2 31136  btwnintr 31132  tgbtwnexch2 25081  tgbtwnintr 25078
[Schwabhauser] p. 30Theorem 3.6btwnexch 31138  btwnexch3 31133  tgbtwnexch 25083  tgbtwnexch3 25079
[Schwabhauser] p. 30Theorem 3.7btwnouttr 31137  tgbtwnouttr 25082  tgbtwnouttr2 25080
[Schwabhauser] p. 32Theorem 3.13axlowdim1 25530
[Schwabhauser] p. 32Theorem 3.14btwndiff 31140  tgbtwndiff 25091
[Schwabhauser] p. 33Theorem 3.17tgtrisegint 25084  trisegint 31141
[Schwabhauser] p. 34Theorem 4.2ifscgr 31157  tgifscgr 25094
[Schwabhauser] p. 34Theorem 4.11colcom 25144  colrot1 25145  colrot2 25146  lncom 25208  lnrot1 25209  lnrot2 25210
[Schwabhauser] p. 34Definition 4.1df-ifs 31153
[Schwabhauser] p. 35Theorem 4.3cgrsub 31158  tgcgrsub 25095
[Schwabhauser] p. 35Theorem 4.5cgrxfr 31168  tgcgrxfr 25104
[Schwabhauser] p. 35Statement 4.4ercgrg 25103
[Schwabhauser] p. 35Definition 4.4df-cgr3 31154  df-cgrg 25097
[Schwabhauser] p. 36Theorem 4.6btwnxfr 31169  tgbtwnxfr 25116
[Schwabhauser] p. 36Theorem 4.11colinearperm1 31175  colinearperm2 31177  colinearperm3 31176  colinearperm4 31178  colinearperm5 31179
[Schwabhauser] p. 36Definition 4.8df-ismt 25119
[Schwabhauser] p. 36Definition 4.10df-colinear 31152  tgellng 25139  tglng 25132
[Schwabhauser] p. 37Theorem 4.12colineartriv1 31180
[Schwabhauser] p. 37Theorem 4.13colinearxfr 31188  lnxfr 25152
[Schwabhauser] p. 37Theorem 4.14lineext 31189  lnext 25153
[Schwabhauser] p. 37Theorem 4.16fscgr 31193  tgfscgr 25154
[Schwabhauser] p. 37Theorem 4.17linecgr 31194  lncgr 25155
[Schwabhauser] p. 37Definition 4.15df-fs 31155
[Schwabhauser] p. 38Theorem 4.18lineid 31196  lnid 25156
[Schwabhauser] p. 38Theorem 4.19idinside 31197  tgidinside 25157
[Schwabhauser] p. 39Theorem 5.1btwnconn1 31214  tgbtwnconn1 25161
[Schwabhauser] p. 41Theorem 5.2btwnconn2 31215  tgbtwnconn2 25162
[Schwabhauser] p. 41Theorem 5.3btwnconn3 31216  tgbtwnconn3 25163
[Schwabhauser] p. 41Theorem 5.5brsegle2 31222
[Schwabhauser] p. 41Definition 5.4df-segle 31220  legov 25171
[Schwabhauser] p. 41Definition 5.5legov2 25172
[Schwabhauser] p. 42Remark 5.13legso 25185
[Schwabhauser] p. 42Theorem 5.6seglecgr12im 31223
[Schwabhauser] p. 42Theorem 5.7seglerflx 31225
[Schwabhauser] p. 42Theorem 5.8segletr 31227
[Schwabhauser] p. 42Theorem 5.9segleantisym 31228
[Schwabhauser] p. 42Theorem 5.10seglelin 31229
[Schwabhauser] p. 42Theorem 5.11seglemin 31226
[Schwabhauser] p. 42Theorem 5.12colinbtwnle 31231
[Schwabhauser] p. 42Proposition 5.7legid 25173
[Schwabhauser] p. 42Proposition 5.8legtrd 25175
[Schwabhauser] p. 42Proposition 5.9legtri3 25176
[Schwabhauser] p. 42Proposition 5.10legtrid 25177
[Schwabhauser] p. 42Proposition 5.11leg0 25178
[Schwabhauser] p. 43Theorem 6.2btwnoutside 31238
[Schwabhauser] p. 43Theorem 6.3broutsideof3 31239
[Schwabhauser] p. 43Theorem 6.4broutsideof 31234  df-outsideof 31233
[Schwabhauser] p. 43Definition 6.1broutsideof2 31235  ishlg 25188
[Schwabhauser] p. 44Theorem 6.4hlln 25193
[Schwabhauser] p. 44Theorem 6.5hlid 25195  outsideofrflx 31240
[Schwabhauser] p. 44Theorem 6.6hlcomb 25189  hlcomd 25190  outsideofcom 31241
[Schwabhauser] p. 44Theorem 6.7hltr 25196  outsideoftr 31242
[Schwabhauser] p. 44Theorem 6.11hlcgreu 25204  outsideofeu 31244
[Schwabhauser] p. 44Definition 6.8df-ray 31251
[Schwabhauser] p. 45Part 2df-lines2 31252
[Schwabhauser] p. 45Theorem 6.13outsidele 31245
[Schwabhauser] p. 45Theorem 6.15lineunray 31260
[Schwabhauser] p. 45Theorem 6.16lineelsb2 31261  tglineelsb2 25218
[Schwabhauser] p. 45Theorem 6.17linecom 31263  linerflx1 31262  linerflx2 31264  tglinecom 25221  tglinerflx1 25219  tglinerflx2 25220
[Schwabhauser] p. 45Theorem 6.18linethru 31266  tglinethru 25222
[Schwabhauser] p. 45Definition 6.14df-line2 31250  tglng 25132
[Schwabhauser] p. 45Proposition 6.13legbtwn 25180
[Schwabhauser] p. 46Theorem 6.19linethrueu 31269  tglinethrueu 25225
[Schwabhauser] p. 46Theorem 6.21lineintmo 31270  tglineineq 25229  tglineinteq 25231  tglineintmo 25228
[Schwabhauser] p. 46Theorem 6.23colline 25235
[Schwabhauser] p. 46Theorem 6.24tglowdim2l 25236
[Schwabhauser] p. 46Theorem 6.25tglowdim2ln 25237
[Schwabhauser] p. 49Theorem 7.3mirinv 25252
[Schwabhauser] p. 49Theorem 7.7mirmir 25248
[Schwabhauser] p. 49Theorem 7.8mirreu3 25240
[Schwabhauser] p. 49Definition 7.5df-mir 25239  ismir 25245  mirbtwn 25244  mircgr 25243  mirfv 25242  mirval 25241
[Schwabhauser] p. 50Theorem 7.8mirreu 25250
[Schwabhauser] p. 50Theorem 7.9mireq 25251
[Schwabhauser] p. 50Theorem 7.10mirinv 25252
[Schwabhauser] p. 50Theorem 7.11mirf1o 25255
[Schwabhauser] p. 50Theorem 7.13miriso 25256
[Schwabhauser] p. 51Theorem 7.14mirmot 25261
[Schwabhauser] p. 51Theorem 7.15mirbtwnb 25258  mirbtwni 25257
[Schwabhauser] p. 51Theorem 7.16mircgrs 25259
[Schwabhauser] p. 51Theorem 7.17miduniq 25271
[Schwabhauser] p. 52Lemma 7.21symquadlem 25275
[Schwabhauser] p. 52Theorem 7.18miduniq1 25272
[Schwabhauser] p. 52Theorem 7.19miduniq2 25273
[Schwabhauser] p. 52Theorem 7.20colmid 25274
[Schwabhauser] p. 53Lemma 7.22krippen 25277
[Schwabhauser] p. 55Lemma 7.25midexlem 25278
[Schwabhauser] p. 57Theorem 8.2ragcom 25284
[Schwabhauser] p. 57Definition 8.1df-rag 25280  israg 25283
[Schwabhauser] p. 58Theorem 8.3ragcol 25285
[Schwabhauser] p. 58Theorem 8.4ragmir 25286
[Schwabhauser] p. 58Theorem 8.5ragtrivb 25288
[Schwabhauser] p. 58Theorem 8.6ragflat2 25289
[Schwabhauser] p. 58Theorem 8.7ragflat 25290
[Schwabhauser] p. 58Theorem 8.8ragtriva 25291
[Schwabhauser] p. 58Theorem 8.9ragflat3 25292  ragncol 25295
[Schwabhauser] p. 58Theorem 8.10ragcgr 25293
[Schwabhauser] p. 59Theorem 8.12perpcom 25299
[Schwabhauser] p. 59Theorem 8.13ragperp 25303
[Schwabhauser] p. 59Theorem 8.14perpneq 25300
[Schwabhauser] p. 59Definition 8.11df-perpg 25282  isperp 25298
[Schwabhauser] p. 59Definition 8.13isperp2 25301
[Schwabhauser] p. 60Theorem 8.18foot 25305
[Schwabhauser] p. 62Lemma 8.20colperpexlem1 25313  colperpexlem2 25314
[Schwabhauser] p. 63Theorem 8.21colperpex 25316  colperpexlem3 25315
[Schwabhauser] p. 64Theorem 8.22mideu 25321  midex 25320
[Schwabhauser] p. 66Lemma 8.24opphllem 25318
[Schwabhauser] p. 67Theorem 9.2oppcom 25327
[Schwabhauser] p. 67Definition 9.1islnopp 25322
[Schwabhauser] p. 68Lemma 9.3opphllem2 25331
[Schwabhauser] p. 68Lemma 9.4opphllem5 25334  opphllem6 25335
[Schwabhauser] p. 69Theorem 9.5opphl 25337
[Schwabhauser] p. 69Theorem 9.6axtgpasch 25056
[Schwabhauser] p. 70Theorem 9.6outpasch 25338
[Schwabhauser] p. 71Theorem 9.8lnopp2hpgb 25346
[Schwabhauser] p. 71Definition 9.7df-hpg 25341  hpgbr 25343
[Schwabhauser] p. 72Lemma 9.10hpgerlem 25348
[Schwabhauser] p. 72Theorem 9.9lnoppnhpg 25347
[Schwabhauser] p. 72Theorem 9.11hpgid 25349
[Schwabhauser] p. 72Theorem 9.12hpgcom 25350
[Schwabhauser] p. 72Theorem 9.13hpgtr 25351
[Schwabhauser] p. 73Theorem 9.18colopp 25352
[Schwabhauser] p. 73Theorem 9.19colhp 25353
[Schwabhauser] p. 88Theorem 10.2lmieu 25367
[Schwabhauser] p. 88Definition 10.1df-mid 25357
[Schwabhauser] p. 89Theorem 10.4lmicom 25371
[Schwabhauser] p. 89Theorem 10.5lmilmi 25372
[Schwabhauser] p. 89Theorem 10.6lmireu 25373
[Schwabhauser] p. 89Theorem 10.7lmieq 25374
[Schwabhauser] p. 89Theorem 10.8lmiinv 25375
[Schwabhauser] p. 89Theorem 10.9lmif1o 25378
[Schwabhauser] p. 89Theorem 10.10lmiiso 25380
[Schwabhauser] p. 89Definition 10.3df-lmi 25358
[Schwabhauser] p. 90Theorem 10.11lmimot 25381
[Schwabhauser] p. 91Theorem 10.12hypcgr 25384
[Schwabhauser] p. 92Theorem 10.14lmiopp 25385
[Schwabhauser] p. 92Theorem 10.15lnperpex 25386
[Schwabhauser] p. 92Theorem 10.16trgcopy 25387  trgcopyeu 25389
[Schwabhauser] p. 95Definition 11.2dfcgra2 25412
[Schwabhauser] p. 95Definition 11.3iscgra 25392
[Schwabhauser] p. 95Proposition 11.4cgracgr 25401
[Schwabhauser] p. 95Proposition 11.10cgrahl1 25399  cgrahl2 25400
[Schwabhauser] p. 96Theorem 11.6cgraid 25402
[Schwabhauser] p. 96Theorem 11.9cgraswap 25403
[Schwabhauser] p. 97Theorem 11.7cgracom 25405
[Schwabhauser] p. 97Theorem 11.8cgratr 25406
[Schwabhauser] p. 97Theorem 11.21cgrabtwn 25408  cgrahl 25409
[Schwabhauser] p. 98Theorem 11.13sacgr 25413
[Schwabhauser] p. 98Theorem 11.14oacgr 25414
[Schwabhauser] p. 98Theorem 11.15acopy 25415  acopyeu 25416
[Schwabhauser] p. 101Theorem 11.24inagswap 25421
[Schwabhauser] p. 101Theorem 11.25inaghl 25422
[Schwabhauser] p. 101Property for point ` ` to lie in the angle ` ` Defnition 11.23isinag 25420
[Schwabhauser] p. 102Lemma 11.28cgrg3col4 25425
[Schwabhauser] p. 102Definition 11.27df-leag 25423  isleag 25424
[Schwabhauser] p. 107Theorem 11.49tgsas 25427  tgsas1 25426  tgsas2 25428  tgsas3 25429
[Schwabhauser] p. 108Theorem 11.50tgasa 25431  tgasa1 25430
[Schwabhauser] p. 109Theorem 11.51tgsss1 25432  tgsss2 25433  tgsss3 25434
[Shapiro] p. 230Theorem 6.5.1dchrhash 24686  dchrsum 24684  dchrsum2 24683  sumdchr 24687
[Shapiro] p. 232Theorem 6.5.2dchr2sum 24688  sum2dchr 24689
[Shapiro], p. 199Lemma 6.1C.2ablfacrp 18193  ablfacrp2 18194
[Shapiro], p. 328Equation 9.2.4vmasum 24631
[Shapiro], p. 329Equation 9.2.7logfac2 24632
[Shapiro], p. 329Equation 9.2.9logfacrlim 24639
[Shapiro], p. 331Equation 9.2.13vmadivsum 24861
[Shapiro], p. 331Equation 9.2.14rplogsumlem2 24864
[Shapiro], p. 336Exercise 9.1.7vmalogdivsum 24918  vmalogdivsum2 24917
[Shapiro], p. 375Theorem 9.4.1dirith 24908  dirith2 24907
[Shapiro], p. 375Equation 9.4.3rplogsum 24906  rpvmasum 24905  rpvmasum2 24891
[Shapiro], p. 376Equation 9.4.7rpvmasumlem 24866
[Shapiro], p. 376Equation 9.4.8dchrvmasum 24904
[Shapiro], p. 377Lemma 9.4.1dchrisum 24871  dchrisumlem1 24868  dchrisumlem2 24869  dchrisumlem3 24870  dchrisumlema 24867
[Shapiro], p. 377Equation 9.4.11dchrvmasumlem1 24874
[Shapiro], p. 379Equation 9.4.16dchrmusum 24903  dchrmusumlem 24901  dchrvmasumlem 24902
[Shapiro], p. 380Lemma 9.4.2dchrmusum2 24873
[Shapiro], p. 380Lemma 9.4.3dchrvmasum2lem 24875
[Shapiro], p. 382Lemma 9.4.4dchrisum0 24899  dchrisum0re 24892  dchrisumn0 24900
[Shapiro], p. 382Equation 9.4.27dchrisum0fmul 24885
[Shapiro], p. 382Equation 9.4.29dchrisum0flb 24889
[Shapiro], p. 383Equation 9.4.30dchrisum0fno1 24890
[Shapiro], p. 403Equation 10.1.16pntrsumbnd 24945  pntrsumbnd2 24946  pntrsumo1 24944
[Shapiro], p. 405Equation 10.2.1mudivsum 24909
[Shapiro], p. 406Equation 10.2.6mulogsum 24911
[Shapiro], p. 407Equation 10.2.7mulog2sumlem1 24913
[Shapiro], p. 407Equation 10.2.8mulog2sum 24916
[Shapiro], p. 418Equation 10.4.6logsqvma 24921
[Shapiro], p. 418Equation 10.4.8logsqvma2 24922
[Shapiro], p. 419Equation 10.4.10selberg 24927
[Shapiro], p. 420Equation 10.4.12selberg2lem 24929
[Shapiro], p. 420Equation 10.4.14selberg2 24930
[Shapiro], p. 422Equation 10.6.7selberg3 24938
[Shapiro], p. 422Equation 10.4.20selberg4lem1 24939
[Shapiro], p. 422Equation 10.4.21selberg3lem1 24936  selberg3lem2 24937
[Shapiro], p. 422Equation 10.4.23selberg4 24940
[Shapiro], p. 427Theorem 10.5.2chpdifbnd 24934
[Shapiro], p. 428Equation 10.6.2selbergr 24947
[Shapiro], p. 429Equation 10.6.8selberg3r 24948
[Shapiro], p. 430Equation 10.6.11selberg4r 24949
[Shapiro], p. 431Equation 10.6.15pntrlog2bnd 24963
[Shapiro], p. 434Equation 10.6.27pntlema 24975  pntlemb 24976  pntlemc 24974  pntlemd 24973  pntlemg 24977
[Shapiro], p. 435Equation 10.6.29pntlema 24975
[Shapiro], p. 436Lemma 10.6.1pntpbnd 24967
[Shapiro], p. 436Lemma 10.6.2pntibnd 24972
[Shapiro], p. 436Equation 10.6.34pntlema 24975
[Shapiro], p. 436Equation 10.6.35pntlem3 24988  pntleml 24990
[Stoll] p. 13Definition corresponds to dfsymdif3 3755
[Stoll] p. 16Exercise 4.40dif 3832  dif0 3807
[Stoll] p. 16Exercise 4.8difdifdir 3911
[Stoll] p. 17Theorem 5.1(5)unvdif 3897
[Stoll] p. 19Theorem 5.2(13)undm 3747
[Stoll] p. 19Theorem 5.2(13')indm 3748
[Stoll] p. 20Remarkinvdif 3730
[Stoll] p. 25Definition of ordered tripledf-ot 4037
[Stoll] p. 43Definitionuniiun 4407
[Stoll] p. 44Definitionintiin 4408
[Stoll] p. 45Definitiondf-iin 4356
[Stoll] p. 45Definition indexed uniondf-iun 4355
[Stoll] p. 176Theorem 3.4(27)iman 438
[Stoll] p. 262Example 4.1dfsymdif3 3755
[Strang] p. 242Section 6.3expgrowth 37438
[Suppes] p. 22Theorem 2eq0 3791  eq0f 3787
[Suppes] p. 22Theorem 4eqss 3487  eqssd 3489  eqssi 3488
[Suppes] p. 23Theorem 5ss0 3829  ss0b 3828
[Suppes] p. 23Theorem 6sstr 3480  sstrALT2 37974
[Suppes] p. 23Theorem 7pssirr 3573
[Suppes] p. 23Theorem 8pssn2lp 3574
[Suppes] p. 23Theorem 9psstr 3577
[Suppes] p. 23Theorem 10pssss 3568
[Suppes] p. 25Theorem 12elin 3662  elun 3619
[Suppes] p. 26Theorem 15inidm 3687
[Suppes] p. 26Theorem 16in0 3823
[Suppes] p. 27Theorem 23unidm 3622
[Suppes] p. 27Theorem 24un0 3822
[Suppes] p. 27Theorem 25ssun1 3642
[Suppes] p. 27Theorem 26ssequn1 3649
[Suppes] p. 27Theorem 27unss 3653
[Suppes] p. 27Theorem 28indir 3737
[Suppes] p. 27Theorem 29undir 3738
[Suppes] p. 28Theorem 32difid 3805
[Suppes] p. 29Theorem 33difin 3726
[Suppes] p. 29Theorem 34indif 3731
[Suppes] p. 29Theorem 35undif1 3898
[Suppes] p. 29Theorem 36difun2 3903
[Suppes] p. 29Theorem 37difin0 3896
[Suppes] p. 29Theorem 38disjdif 3895
[Suppes] p. 29Theorem 39difundi 3741
[Suppes] p. 29Theorem 40difindi 3743
[Suppes] p. 30Theorem 41nalset 4622
[Suppes] p. 39Theorem 61uniss 4292
[Suppes] p. 39Theorem 65uniop 4797
[Suppes] p. 41Theorem 70intsn 4346
[Suppes] p. 42Theorem 71intpr 4343  intprg 4344
[Suppes] p. 42Theorem 73op1stb 4765
[Suppes] p. 42Theorem 78intun 4342
[Suppes] p. 44Definition 15(a)dfiun2 4388  dfiun2g 4386
[Suppes] p. 44Definition 15(b)dfiin2 4389
[Suppes] p. 47Theorem 86elpw 4017  elpw2 4654  elpw2g 4653  elpwg 4019  elpwgdedVD 38057
[Suppes] p. 47Theorem 87pwid 4025
[Suppes] p. 47Theorem 89pw0 4186
[Suppes] p. 48Theorem 90pwpw0 4187
[Suppes] p. 52Theorem 101xpss12 5041
[Suppes] p. 52Theorem 102xpindi 5069  xpindir 5070
[Suppes] p. 52Theorem 103xpundi 4988  xpundir 4989
[Suppes] p. 54Theorem 105elirrv 8262
[Suppes] p. 58Theorem 2relss 5023
[Suppes] p. 59Theorem 4eldm 5134  eldm2 5135  eldm2g 5133  eldmg 5132
[Suppes] p. 59Definition 3df-dm 4942
[Suppes] p. 60Theorem 6dmin 5145
[Suppes] p. 60Theorem 8rnun 5350
[Suppes] p. 60Theorem 9rnin 5351
[Suppes] p. 60Definition 4dfrn2 5125
[Suppes] p. 61Theorem 11brcnv 5119  brcnvg 5117
[Suppes] p. 62Equation 5elcnv 5113  elcnv2 5114
[Suppes] p. 62Theorem 12relcnv 5313
[Suppes] p. 62Theorem 15cnvin 5349
[Suppes] p. 62Theorem 16cnvun 5347
[Suppes] p. 63Theorem 20co02 5456
[Suppes] p. 63Theorem 21dmcoss 5197
[Suppes] p. 63Definition 7df-co 4941
[Suppes] p. 64Theorem 26cnvco 5122
[Suppes] p. 64Theorem 27coass 5461
[Suppes] p. 65Theorem 31resundi 5221
[Suppes] p. 65Theorem 34elima 5280  elima2 5281  elima3 5282  elimag 5279
[Suppes] p. 65Theorem 35imaundi 5354
[Suppes] p. 66Theorem 40dminss 5356
[Suppes] p. 66Theorem 41imainss 5357
[Suppes] p. 67Exercise 11cnvxp 5360
[Suppes] p. 81Definition 34dfec2 7507
[Suppes] p. 82Theorem 72elec 7548  elecg 7547
[Suppes] p. 82Theorem 73erth 7553  erth2 7554
[Suppes] p. 83Theorem 74erdisj 7556
[Suppes] p. 89Theorem 96map0b 7657
[Suppes] p. 89Theorem 97map0 7659  map0g 7658
[Suppes] p. 89Theorem 98mapsn 7660
[Suppes] p. 89Theorem 99mapss 7661
[Suppes] p. 91Definition 12(ii)alephsuc 8649
[Suppes] p. 91Definition 12(iii)alephlim 8648
[Suppes] p. 92Theorem 1enref 7749  enrefg 7748
[Suppes] p. 92Theorem 2ensym 7766  ensymb 7765  ensymi 7767
[Suppes] p. 92Theorem 3entr 7769
[Suppes] p. 92Theorem 4unen 7800
[Suppes] p. 94Theorem 15endom 7743
[Suppes] p. 94Theorem 16ssdomg 7762
[Suppes] p. 94Theorem 17domtr 7770
[Suppes] p. 95Theorem 18sbth 7840
[Suppes] p. 97Theorem 23canth2 7873  canth2g 7874
[Suppes] p. 97Definition 3brsdom2 7844  df-sdom 7719  dfsdom2 7843
[Suppes] p. 97Theorem 21(i)sdomirr 7857
[Suppes] p. 97Theorem 22(i)domnsym 7846
[Suppes] p. 97Theorem 21(ii)sdomnsym 7845
[Suppes] p. 97Theorem 22(ii)domsdomtr 7855
[Suppes] p. 97Theorem 22(iv)brdom2 7746
[Suppes] p. 97Theorem 21(iii)sdomtr 7858
[Suppes] p. 97Theorem 22(iii)sdomdomtr 7853
[Suppes] p. 98Exercise 4fundmen 7791  fundmeng 7792
[Suppes] p. 98Exercise 6xpdom3 7818
[Suppes] p. 98Exercise 11sdomentr 7854
[Suppes] p. 104Theorem 37fofi 8010
[Suppes] p. 104Theorem 38pwfi 8019
[Suppes] p. 105Theorem 40pwfi 8019
[Suppes] p. 111Axiom for cardinal numberscarden 9127
[Suppes] p. 130Definition 3df-tr 4579
[Suppes] p. 132Theorem 9ssonuni 6753
[Suppes] p. 134Definition 6df-suc 5536
[Suppes] p. 136Theorem Schema 22findes 6863  finds 6859  finds1 6862  finds2 6861
[Suppes] p. 151Theorem 42isfinite 8307  isfinite2 7978  isfiniteg 7980  unbnn 7976
[Suppes] p. 162Definition 5df-ltnq 9494  df-ltpq 9486
[Suppes] p. 197Theorem Schema 4tfindes 6829  tfinds 6826  tfinds2 6830
[Suppes] p. 209Theorem 18oaord1 7393
[Suppes] p. 209Theorem 21oaword2 7395
[Suppes] p. 211Theorem 25oaass 7403
[Suppes] p. 225Definition 8iscard2 8560
[Suppes] p. 227Theorem 56ondomon 9139
[Suppes] p. 228Theorem 59harcard 8562
[Suppes] p. 228Definition 12(i)aleph0 8647
[Suppes] p. 228Theorem Schema 61onintss 5580
[Suppes] p. 228Theorem Schema 62onminesb 6765  onminsb 6766
[Suppes] p. 229Theorem 64alephval2 9148
[Suppes] p. 229Theorem 65alephcard 8651
[Suppes] p. 229Theorem 66alephord2i 8658
[Suppes] p. 229Theorem 67alephnbtwn 8652
[Suppes] p. 229Definition 12df-aleph 8524
[Suppes] p. 242Theorem 6weth 9075
[Suppes] p. 242Theorem 8entric 9133
[Suppes] p. 242Theorem 9carden 9127
[TakeutiZaring] p. 8Axiom 1ax-ext 2494
[TakeutiZaring] p. 13Definition 4.5df-cleq 2507
[TakeutiZaring] p. 13Proposition 4.6df-clel 2510
[TakeutiZaring] p. 13Proposition 4.9cvjust 2509
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2533
[TakeutiZaring] p. 14Definition 4.16df-oprab 6429
[TakeutiZaring] p. 14Proposition 4.14ru 3305
[TakeutiZaring] p. 15Axiom 2zfpair 4730
[TakeutiZaring] p. 15Exercise 1elpr 4049  elpr2 4050  elprg 4047
[TakeutiZaring] p. 15Exercise 2elsn 4043  elsn2 4061  elsn2g 4060  elsng 4042  velsn 4044
[TakeutiZaring] p. 15Exercise 3elop 4760
[TakeutiZaring] p. 15Exercise 4sneq 4038  sneqr 4210
[TakeutiZaring] p. 15Definition 5.1dfpr2 4046  dfsn2 4041
[TakeutiZaring] p. 16Axiom 3uniex 6726
[TakeutiZaring] p. 16Exercise 6opth 4769
[TakeutiZaring] p. 16Exercise 7opex 4757
[TakeutiZaring] p. 16Exercise 8rext 4741
[TakeutiZaring] p. 16Corollary 5.8unex 6729  unexg 6732
[TakeutiZaring] p. 16Definition 5.3dftp2 4081
[TakeutiZaring] p. 16Definition 5.5df-uni 4271
[TakeutiZaring] p. 16Definition 5.6df-in 3451  df-un 3449
[TakeutiZaring] p. 16Proposition 5.7unipr 4283  uniprg 4284
[TakeutiZaring] p. 17Axiom 4pwex 4673  pwexg 4675
[TakeutiZaring] p. 17Exercise 1eltp 4080
[TakeutiZaring] p. 17Exercise 5elsuc 5599  elsucg 5597  sstr2 3479
[TakeutiZaring] p. 17Exercise 6uncom 3623
[TakeutiZaring] p. 17Exercise 7incom 3670
[TakeutiZaring] p. 17Exercise 8unass 3636
[TakeutiZaring] p. 17Exercise 9inass 3688
[TakeutiZaring] p. 17Exercise 10indi 3735
[TakeutiZaring] p. 17Exercise 11undi 3736
[TakeutiZaring] p. 17Definition 5.9df-pss 3460  dfss2 3461
[TakeutiZaring] p. 17Definition 5.10df-pw 4013
[TakeutiZaring] p. 18Exercise 7unss2 3650
[TakeutiZaring] p. 18Exercise 9df-ss 3458  sseqin2 3682
[TakeutiZaring] p. 18Exercise 10ssid 3491
[TakeutiZaring] p. 18Exercise 12inss1 3698  inss2 3699
[TakeutiZaring] p. 18Exercise 13nss 3530
[TakeutiZaring] p. 18Exercise 15unieq 4278
[TakeutiZaring] p. 18Exercise 18sspwb 4742  sspwimp 38058  sspwimpALT 38065  sspwimpALT2 38068  sspwimpcf 38060
[TakeutiZaring] p. 18Exercise 19pweqb 4750
[TakeutiZaring] p. 19Axiom 5ax-rep 4597
[TakeutiZaring] p. 20Definitiondf-rab 2809
[TakeutiZaring] p. 20Corollary 5.160ex 4617
[TakeutiZaring] p. 20Definition 5.12df-dif 3447
[TakeutiZaring] p. 20Definition 5.14dfnul2 3779
[TakeutiZaring] p. 20Proposition 5.15difid 3805
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3793  n0f 3789  neq0 3792  neq0f 3788
[TakeutiZaring] p. 21Axiom 6zfreg 8258
[TakeutiZaring] p. 21Axiom 6'zfregs 8366
[TakeutiZaring] p. 21Theorem 5.22setind 8368
[TakeutiZaring] p. 21Definition 5.20df-v 3079
[TakeutiZaring] p. 21Proposition 5.21vprc 4623
[TakeutiZaring] p. 22Exercise 10ss 3827
[TakeutiZaring] p. 22Exercise 3ssex 4629  ssexg 4631
[TakeutiZaring] p. 22Exercise 4inex1 4626
[TakeutiZaring] p. 22Exercise 5ruv 8265
[TakeutiZaring] p. 22Exercise 6elirr 8263
[TakeutiZaring] p. 22Exercise 7ssdif0 3799
[TakeutiZaring] p. 22Exercise 11difdif 3602
[TakeutiZaring] p. 22Exercise 13undif3 3750  undif3VD 38022
[TakeutiZaring] p. 22Exercise 14difss 3603
[TakeutiZaring] p. 22Exercise 15sscon 3610
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2805
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2806
[TakeutiZaring] p. 23Proposition 6.2xpex 6735  xpexg 6733
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4939
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5759
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5905  fun11 5762
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5701  svrelfun 5760
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 5124
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 5126
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4944
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4945
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4941
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5397  dfrel2 5392
[TakeutiZaring] p. 25Exercise 3xpss 5042
[TakeutiZaring] p. 25Exercise 5relun 5051
[TakeutiZaring] p. 25Exercise 6reluni 5057
[TakeutiZaring] p. 25Exercise 9inxp 5068
[TakeutiZaring] p. 25Exercise 12relres 5237
[TakeutiZaring] p. 25Exercise 13opelres 5213  opelresg 5215
[TakeutiZaring] p. 25Exercise 14dmres 5230
[TakeutiZaring] p. 25Exercise 15resss 5233
[TakeutiZaring] p. 25Exercise 17resabs1 5238
[TakeutiZaring] p. 25Exercise 18funres 5728
[TakeutiZaring] p. 25Exercise 24relco 5440
[TakeutiZaring] p. 25Exercise 29funco 5727
[TakeutiZaring] p. 25Exercise 30f1co 5906
[TakeutiZaring] p. 26Definition 6.10eu2 2401
[TakeutiZaring] p. 26Definition 6.11conventions 26389  df-fv 5697  fv3 5999
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 6880  cnvexg 6879
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 6866  dmexg 6864
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 6867  rnexg 6865
[TakeutiZaring] p. 26Corollary 6.9(1)xpexb 37561
[TakeutiZaring] p. 26Corollary 6.9(2)xpexcnv 6875
[TakeutiZaring] p. 27Corollary 6.13fvex 5996
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1-afv 39798  tz6.12-1 6003  tz6.12-afv 39797  tz6.12 6004  tz6.12c 6006
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5977  tz6.12i 6007
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5692
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5693
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5695  wfo 5687
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5694  wf1 5686
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5696  wf1o 5688
[TakeutiZaring] p. 28Exercise 4eqfnfv 6102  eqfnfv2 6103  eqfnfv2f 6106
[TakeutiZaring] p. 28Exercise 5fvco 6067
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 6262
[TakeutiZaring] p. 28Proposition 6.17resfunexg 6260
[TakeutiZaring] p. 29Exercise 9funimaex 5775  funimaexg 5774
[TakeutiZaring] p. 29Definition 6.18df-br 4482
[TakeutiZaring] p. 29Definition 6.19(1)df-so 4854
[TakeutiZaring] p. 30Definition 6.21dffr2 4897  dffr3 5308  eliniseg 5304  iniseg 5306
[TakeutiZaring] p. 30Definition 6.22df-eprel 4843
[TakeutiZaring] p. 30Proposition 6.23fr2nr 4910  fr3nr 6746  frirr 4909
[TakeutiZaring] p. 30Definition 6.24(1)df-fr 4891
[TakeutiZaring] p. 30Definition 6.24(2)dfwe2 6748
[TakeutiZaring] p. 31Exercise 1frss 4899
[TakeutiZaring] p. 31Exercise 4wess 4919
[TakeutiZaring] p. 31Proposition 6.26tz6.26 5518  tz6.26i 5519  wefrc 4926  wereu2 4929
[TakeutiZaring] p. 32Theorem 6.27wfi 5520  wfii 5521
[TakeutiZaring] p. 32Definition 6.28df-isom 5698
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 6355
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 6356
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 6362
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 6363
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 6364
[TakeutiZaring] p. 33Proposition 6.32(1)isofr 6368
[TakeutiZaring] p. 33Proposition 6.32(3)isowe 6375
[TakeutiZaring] p. 34Proposition 6.33f1oiso 6377
[TakeutiZaring] p. 35Notationwtr 4578
[TakeutiZaring] p. 35Theorem 7.2trelpss 37562  tz7.2 4916
[TakeutiZaring] p. 35Definition 7.1dftr3 4582
[TakeutiZaring] p. 36Proposition 7.4ordwe 5543
[TakeutiZaring] p. 36Proposition 7.5tz7.5 5551
[TakeutiZaring] p. 36Proposition 7.6ordelord 5552  ordelordALT 37650  ordelordALTVD 38007
[TakeutiZaring] p. 37Corollary 7.8ordelpss 5558  ordelssne 5557
[TakeutiZaring] p. 37Proposition 7.7tz7.7 5556
[TakeutiZaring] p. 37Proposition 7.9ordin 5560
[TakeutiZaring] p. 38Corollary 7.14ordeleqon 6755
[TakeutiZaring] p. 38Corollary 7.15ordsson 6756
[TakeutiZaring] p. 38Definition 7.11df-on 5534
[TakeutiZaring] p. 38Proposition 7.10ordtri3or 5562
[TakeutiZaring] p. 38Proposition 7.12onfrALT 37667  ordon 6749
[TakeutiZaring] p. 38Proposition 7.13onprc 6751
[TakeutiZaring] p. 39Theorem 7.17tfi 6820
[TakeutiZaring] p. 40Exercise 3ontr2 5577
[TakeutiZaring] p. 40Exercise 7dftr2 4580
[TakeutiZaring] p. 40Exercise 9onssmin 6764
[TakeutiZaring] p. 40Exercise 11unon 6798
[TakeutiZaring] p. 40Exercise 12ordun 5631
[TakeutiZaring] p. 40Exercise 14ordequn 5630
[TakeutiZaring] p. 40Proposition 7.19ssorduni 6752
[TakeutiZaring] p. 40Proposition 7.20elssuni 4301
[TakeutiZaring] p. 41Definition 7.22df-suc 5536
[TakeutiZaring] p. 41Proposition 7.23sssucid 5607  sucidg 5608
[TakeutiZaring] p. 41Proposition 7.24suceloni 6780
[TakeutiZaring] p. 41Proposition 7.25onnbtwn 5621  ordnbtwn 5620
[TakeutiZaring] p. 41Proposition 7.26onsucuni 6795
[TakeutiZaring] p. 42Exercise 1df-lim 5535
[TakeutiZaring] p. 42Exercise 4omssnlim 6846
[TakeutiZaring] p. 42Exercise 7ssnlim 6850
[TakeutiZaring] p. 42Exercise 8onsucssi 6808  ordelsuc 6787
[TakeutiZaring] p. 42Exercise 9ordsucelsuc 6789
[TakeutiZaring] p. 42Definition 7.27nlimon 6818
[TakeutiZaring] p. 42Definition 7.28dfom2 6834
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 6852
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 6853
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 6854
[TakeutiZaring] p. 43Remarkomon 6843
[TakeutiZaring] p. 43Axiom 7inf3 8290  omex 8298
[TakeutiZaring] p. 43Theorem 7.32ordom 6841
[TakeutiZaring] p. 43Corollary 7.31find 6858
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 6855
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 6856
[TakeutiZaring] p. 44Exercise 1limomss 6837
[TakeutiZaring] p. 44Exercise 2int0 4323  trint0 4596
[TakeutiZaring] p. 44Exercise 4intss1 4325
[TakeutiZaring] p. 44Exercise 5intex 4646
[TakeutiZaring] p. 44Exercise 6oninton 6767
[TakeutiZaring] p. 44Exercise 11ordintdif 5579
[TakeutiZaring] p. 44Definition 7.35df-int 4309
[TakeutiZaring] p. 44Proposition 7.34noinfep 8315
[TakeutiZaring] p. 45Exercise 4onint 6762
[TakeutiZaring] p. 47Lemma 1tfrlem1 7234
[TakeutiZaring] p. 47Theorem 7.41(1)tfr1 7255
[TakeutiZaring] p. 47Theorem 7.41(2)tfr2 7256
[TakeutiZaring] p. 47Theorem 7.41(3)tfr3 7257
[TakeutiZaring] p. 49Theorem 7.44tz7.44-1 7264  tz7.44-2 7265  tz7.44-3 7266
[TakeutiZaring] p. 50Exercise 1smogt 7226
[TakeutiZaring] p. 50Exercise 3smoiso 7221
[TakeutiZaring] p. 50Definition 7.46df-smo 7205
[TakeutiZaring] p. 51Proposition 7.49tz7.49 7302  tz7.49c 7303
[TakeutiZaring] p. 51Proposition 7.48(1)tz7.48-1 7300
[TakeutiZaring] p. 51Proposition 7.48(2)tz7.48-2 7299
[TakeutiZaring] p. 51Proposition 7.48(3)tz7.48-3 7301
[TakeutiZaring] p. 53Proposition 7.532eu5 2449
[TakeutiZaring] p. 54Proposition 7.56(1)leweon 8592
[TakeutiZaring] p. 54Proposition 7.58(1)r0weon 8593
[TakeutiZaring] p. 56Definition 8.1oalim 7374  oasuc 7366
[TakeutiZaring] p. 57Remarktfindsg 6827
[TakeutiZaring] p. 57Proposition 8.2oacl 7377
[TakeutiZaring] p. 57Proposition 8.3oa0 7358  oa0r 7380
[TakeutiZaring] p. 57Proposition 8.16omcl 7378
[TakeutiZaring] p. 58Corollary 8.5oacan 7390
[TakeutiZaring] p. 58Proposition 8.4nnaord 7461  nnaordi 7460  oaord 7389  oaordi 7388
[TakeutiZaring] p. 59Proposition 8.6iunss2 4399  uniss2 4304
[TakeutiZaring] p. 59Proposition 8.7oawordri 7392
[TakeutiZaring] p. 59Proposition 8.8oawordeu 7397  oawordex 7399
[TakeutiZaring] p. 59Proposition 8.9nnacl 7453
[TakeutiZaring] p. 59Proposition 8.10oaabs 7486
[TakeutiZaring] p. 60Remarkoancom 8306
[TakeutiZaring] p. 60Proposition 8.11oalimcl 7402
[TakeutiZaring] p. 62Exercise 1nnarcl 7458
[TakeutiZaring] p. 62Exercise 5oaword1 7394
[TakeutiZaring] p. 62Definition 8.15om0 7359  om0x 7361  omlim 7375  omsuc 7368
[TakeutiZaring] p. 63Proposition 8.17nnecl 7455  nnmcl 7454
[TakeutiZaring] p. 63Proposition 8.19nnmord 7474  nnmordi 7473  omord 7410  omordi 7408
[TakeutiZaring] p. 63Proposition 8.20omcan 7411
[TakeutiZaring] p. 63Proposition 8.21nnmwordri 7478  omwordri 7414
[TakeutiZaring] p. 63Proposition 8.18(1)om0r 7381
[TakeutiZaring] p. 63Proposition 8.18(2)om1 7384  om1r 7385
[TakeutiZaring] p. 64Proposition 8.22om00 7417
[TakeutiZaring] p. 64Proposition 8.23omordlim 7419
[TakeutiZaring] p. 64Proposition 8.24omlimcl 7420
[TakeutiZaring] p. 64Proposition 8.25odi 7421
[TakeutiZaring] p. 65Theorem 8.26omass 7422
[TakeutiZaring] p. 67Definition 8.30nnesuc 7450  oe0 7364  oelim 7376  oesuc 7369  onesuc 7372
[TakeutiZaring] p. 67Proposition 8.31oe0m0 7362
[TakeutiZaring] p. 67Proposition 8.32oen0 7428
[TakeutiZaring] p. 67Proposition 8.33oeordi 7429
[TakeutiZaring] p. 67Proposition 8.31(2)oe0m1 7363
[TakeutiZaring] p. 67Proposition 8.31(3)oe1m 7387
[TakeutiZaring] p. 68Corollary 8.34oeord 7430
[TakeutiZaring] p. 68Corollary 8.36oeordsuc 7436
[TakeutiZaring] p. 68Proposition 8.35oewordri 7434
[TakeutiZaring] p. 68Proposition 8.37oeworde 7435
[TakeutiZaring] p. 69Proposition 8.41oeoa 7439
[TakeutiZaring] p. 70Proposition 8.42oeoe 7441
[TakeutiZaring] p. 73Theorem 9.1trcl 8362  tz9.1 8363
[TakeutiZaring] p. 76Definition 9.9df-r1 8385  r10 8389  r1lim 8393  r1limg 8392  r1suc 8391  r1sucg 8390
[TakeutiZaring] p. 77Proposition 9.10(2)r1ord 8401  r1ord2 8402  r1ordg 8399
[TakeutiZaring] p. 78Proposition 9.12tz9.12 8411
[TakeutiZaring] p. 78Proposition 9.13rankwflem 8436  tz9.13 8412  tz9.13g 8413
[TakeutiZaring] p. 79Definition 9.14df-rank 8386  rankval 8437  rankvalb 8418  rankvalg 8438
[TakeutiZaring] p. 79Proposition 9.16rankel 8460  rankelb 8445
[TakeutiZaring] p. 79Proposition 9.17rankuni2b 8474  rankval3 8461  rankval3b 8447
[TakeutiZaring] p. 79Proposition 9.18rankonid 8450
[TakeutiZaring] p. 79Proposition 9.15(1)rankon 8416
[TakeutiZaring] p. 79Proposition 9.15(2)rankr1 8455  rankr1c 8442  rankr1g 8453
[TakeutiZaring] p. 79Proposition 9.15(3)ssrankr1 8456
[TakeutiZaring] p. 80Exercise 1rankss 8470  rankssb 8469
[TakeutiZaring] p. 80Exercise 2unbndrank 8463
[TakeutiZaring] p. 80Proposition 9.19bndrank 8462
[TakeutiZaring] p. 83Axiom of Choiceac4 9055  dfac3 8702
[TakeutiZaring] p. 84Theorem 10.3dfac8a 8611  numth 9052  numth2 9051
[TakeutiZaring] p. 85Definition 10.4cardval 9122
[TakeutiZaring] p. 85Proposition 10.5cardid 9123  cardid2 8537
[TakeutiZaring] p. 85Proposition 10.9oncard 8544
[TakeutiZaring] p. 85Proposition 10.10carden 9127
[TakeutiZaring] p. 85Proposition 10.11cardidm 8543
[TakeutiZaring] p. 85Proposition 10.6(1)cardon 8528
[TakeutiZaring] p. 85Proposition 10.6(2)cardne 8549
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 8541
[TakeutiZaring] p. 87Proposition 10.15pwen 7893
[TakeutiZaring] p. 88Exercise 1en0 7780
[TakeutiZaring] p. 88Exercise 7infensuc 7898
[TakeutiZaring] p. 89Exercise 10omxpen 7822
[TakeutiZaring] p. 90Corollary 10.23cardnn 8547
[TakeutiZaring] p. 90Definition 10.27alephiso 8679
[TakeutiZaring] p. 90Proposition 10.20nneneq 7903
[TakeutiZaring] p. 90Proposition 10.22onomeneq 7910
[TakeutiZaring] p. 90Proposition 10.26alephprc 8680
[TakeutiZaring] p. 90Corollary 10.21(1)php5 7908
[TakeutiZaring] p. 91Exercise 2alephle 8669
[TakeutiZaring] p. 91Exercise 3aleph0 8647
[TakeutiZaring] p. 91Exercise 4cardlim 8556
[TakeutiZaring] p. 91Exercise 7infpss 8797
[TakeutiZaring] p. 91Exercise 8infcntss 7994
[TakeutiZaring] p. 91Definition 10.29df-fin 7720  isfi 7740
[TakeutiZaring] p. 92Proposition 10.32onfin 7911
[TakeutiZaring] p. 92Proposition 10.34imadomg 9112
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 7815
[TakeutiZaring] p. 93Proposition 10.35fodomb 9104
[TakeutiZaring] p. 93Proposition 10.36cdaxpdom 8769  unxpdom 7927
[TakeutiZaring] p. 93Proposition 10.37cardsdomel 8558  cardsdomelir 8557
[TakeutiZaring] p. 93Proposition 10.38sucxpdom 7929
[TakeutiZaring] p. 94Proposition 10.39infxpen 8595
[TakeutiZaring] p. 95Definition 10.42df-map 7621
[TakeutiZaring] p. 95Proposition 10.40infxpidm 9138  infxpidm2 8598
[TakeutiZaring] p. 95Proposition 10.41infcda 8788  infxp 8795
[TakeutiZaring] p. 96Proposition 10.44pw2en 7827  pw2f1o 7825
[TakeutiZaring] p. 96Proposition 10.45mapxpen 7886
[TakeutiZaring] p. 97Theorem 10.46ac6s3 9067
[TakeutiZaring] p. 98Theorem 10.46ac6c5 9062  ac6s5 9071
[TakeutiZaring] p. 98Theorem 10.47unidom 9119
[TakeutiZaring] p. 99Theorem 10.48uniimadom 9120  uniimadomf 9121
[TakeutiZaring] p. 100Definition 11.1cfcof 8854
[TakeutiZaring] p. 101Proposition 11.7cofsmo 8849
[TakeutiZaring] p. 102Exercise 1cfle 8834
[TakeutiZaring] p. 102Exercise 2cf0 8831
[TakeutiZaring] p. 102Exercise 3cfsuc 8837
[TakeutiZaring] p. 102Exercise 4cfom 8844
[TakeutiZaring] p. 102Proposition 11.9coftr 8853
[TakeutiZaring] p. 103Theorem 11.15alephreg 9158
[TakeutiZaring] p. 103Proposition 11.11cardcf 8832
[TakeutiZaring] p. 103Proposition 11.13alephsing 8856
[TakeutiZaring] p. 104Corollary 11.17cardinfima 8678
[TakeutiZaring] p. 104Proposition 11.16carduniima 8677
[TakeutiZaring] p. 104Proposition 11.18alephfp 8689  alephfp2 8690
[TakeutiZaring] p. 106Theorem 11.20gchina 9275
[TakeutiZaring] p. 106Theorem 11.21mappwen 8693
[TakeutiZaring] p. 107Theorem 11.26konigth 9145
[TakeutiZaring] p. 108Theorem 11.28pwcfsdom 9159
[TakeutiZaring] p. 108Theorem 11.29cfpwsdom 9160
[Tarski] p. 67Axiom B5ax-c5 33061
[Tarski] p. 67Scheme B5sp 1990
[Tarski] p. 68Lemma 6avril1 26450  equid 1889
[Tarski] p. 69Lemma 7equcomi 1894
[Tarski] p. 70Lemma 14spim 2145  spime 2147  spimeh 1875
[Tarski] p. 70Lemma 16ax-12 1983  ax-c15 33067  ax12i 1829
[Tarski] p. 70Lemmas 16 and 17sb6 2321
[Tarski] p. 75Axiom B7ax6v 1839
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-5 1793  ax5ALT 33085
[Tarski], p. 75Scheme B8 of system S2ax-7 1885  ax-8 1940  ax-9 1947
[Tarski1999] p. 178Axiom 4axtgsegcon 25053
[Tarski1999] p. 178Axiom 5axtg5seg 25054
[Tarski1999] p. 179Axiom 7axtgpasch 25056
[Tarski1999] p. 180Axiom 7.1axtgpasch 25056
[Tarski1999] p. 185Axiom 11axtgcont1 25057
[Truss] p. 114Theorem 5.18ruc 14678
[Viaclovsky7] p. 3Corollary 0.3mblfinlem3 32493
[Viaclovsky8] p. 3Proposition 7ismblfin 32495
[Weierstrass] p. 272Definitiondf-mdet 20111  mdetuni 20148
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 533
[WhiteheadRussell] p. 96Axiom *1.3olc 397
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 399
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 542
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 881
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 178
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 128
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 87  wl-pm2.04 32275
[WhiteheadRussell] p. 100Theorem *2.05frege5 36996  imim2 55  wl-imim2 32270
[WhiteheadRussell] p. 100Theorem *2.06imim1 80
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 431
[WhiteheadRussell] p. 101Theorem *2.06barbara 2455  syl 17
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 409
[WhiteheadRussell] p. 101Theorem *2.08id 22  wl-id 32273
[WhiteheadRussell] p. 101Theorem *2.11exmid 429
[WhiteheadRussell] p. 101Theorem *2.12notnot 134
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 432
[WhiteheadRussell] p. 102Theorem *2.14notnotr 123  notnotrALT2 38067  wl-notnotr 32274
[WhiteheadRussell] p. 102Theorem *2.15con1 141
[WhiteheadRussell] p. 103Theorem *2.16ax-frege28 37026  axfrege28 37025  con3 147
[WhiteheadRussell] p. 103Theorem *2.17ax-3 8
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 120
[WhiteheadRussell] p. 104Theorem *2.2orc 398
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 593
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 118  wl-pm2.21 32267
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 119
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 417
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 922
[WhiteheadRussell] p. 104Theorem *2.27conventions-label 26390  pm2.27 40  wl-pm2.27 32265
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 545
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 546
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 883
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 884
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 882
[WhiteheadRussell] p. 105Definition *2.33df-3or 1031
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 596
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 594
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 595
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 53
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 410
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 411
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 162
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 180
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 412
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 413
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 414
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 163
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 165
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 386
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 387
[WhiteheadRussell] p. 107Theorem *2.55orel1 395
[WhiteheadRussell] p. 107Theorem *2.56orel2 396
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 181
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 423
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 824
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 825
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 182
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 415  pm2.67 416
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 164
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 422
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 890
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 424
[WhiteheadRussell] p. 108Theorem *2.69looinv 192
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 885
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 886
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 889
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 888
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 891
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 892
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 81
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 893
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 105
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 517
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 461  pm3.2im 155
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 518
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 519
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 520
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 521
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 462
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 463
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 921
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 608
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 458
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 459
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 471  simplim 161
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 475  simprim 160
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 606
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 607
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 600
[WhiteheadRussell] p. 113Fact)pm3.45 874
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 581
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 579
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 580
[WhiteheadRussell] p. 113Theorem *3.44jao 532  pm3.44 531
[WhiteheadRussell] p. 113Theorem *3.47prth 592
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 901
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 873
[WhiteheadRussell] p. 116Theorem *4.1con34b 304
[WhiteheadRussell] p. 117Theorem *4.2biid 249
[WhiteheadRussell] p. 117Theorem *4.11notbi 307
[WhiteheadRussell] p. 117Theorem *4.12con2bi 341
[WhiteheadRussell] p. 117Theorem *4.13notnotb 302
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 599
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 602
[WhiteheadRussell] p. 117Theorem *4.21bicom 210
[WhiteheadRussell] p. 117Theorem *4.22biantr 967  bitr 740
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 672
[WhiteheadRussell] p. 117Theorem *4.25oridm 534  pm4.25 535
[WhiteheadRussell] p. 118Theorem *4.3ancom 464
[WhiteheadRussell] p. 118Theorem *4.4andi 906
[WhiteheadRussell] p. 118Theorem *4.31orcom 400
[WhiteheadRussell] p. 118Theorem *4.32anass 678
[WhiteheadRussell] p. 118Theorem *4.33orass 544
[WhiteheadRussell] p. 118Theorem *4.36anbi1 738
[WhiteheadRussell] p. 118Theorem *4.37orbi1 737
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 911
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 910
[WhiteheadRussell] p. 118Definition *4.34df-3an 1032
[WhiteheadRussell] p. 119Theorem *4.41ordi 903
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 994
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 963
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 598
[WhiteheadRussell] p. 119Theorem *4.45orabs 895  pm4.45 719  pm4.45im 582
[WhiteheadRussell] p. 120Theorem *4.5anor 508
[WhiteheadRussell] p. 120Theorem *4.6imor 426
[WhiteheadRussell] p. 120Theorem *4.7anclb 567
[WhiteheadRussell] p. 120Theorem *4.51ianor 507
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 510
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 511
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 512
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 513
[WhiteheadRussell] p. 120Theorem *4.56ioran 509  pm4.56 514
[WhiteheadRussell] p. 120Theorem *4.57oran 515  pm4.57 516
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 440
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 433
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 435
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 385
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 441
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 434
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 442
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 659  pm4.71d 663  pm4.71i 661  pm4.71r 660  pm4.71rd 664  pm4.71ri 662
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 915
[WhiteheadRussell] p. 121Theorem *4.73iba 522
[WhiteheadRussell] p. 121Theorem *4.74biorf 418
[WhiteheadRussell] p. 121Theorem *4.76jcab 902  pm4.76 905
[WhiteheadRussell] p. 121Theorem *4.77jaob 817  pm4.77 823
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 603
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 604
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 378
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 379
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 964
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 965
[WhiteheadRussell] p. 122Theorem *4.84imbi1 335
[WhiteheadRussell] p. 122Theorem *4.85imbi2 336
[WhiteheadRussell] p. 122Theorem *4.86bibi1 339
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 374  impexp 460  pm4.87 605
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 897
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 923
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 924
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 926
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 925
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 928
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 929
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 927
[WhiteheadRussell] p. 124Theorem *5.18nbbn 371  pm5.18 369
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 373
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 898
[WhiteheadRussell] p. 124Theorem *5.22xor 930
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 932
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 933
[WhiteheadRussell] p. 124Theorem *5.25dfor2 425
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 743
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 375
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 349
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 948
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 970
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 609
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 665
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 917
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 939
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 918
[WhiteheadRussell] p. 125Theorem *5.41imdi 376  pm5.41 377
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 568
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 947
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 832
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 940
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 936
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 744
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 959
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 960
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 972
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 354
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 257
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 973
[WhiteheadRussell] p. 146Theorem *10.12pm10.12 37461
[WhiteheadRussell] p. 146Theorem *10.14pm10.14 37462
[WhiteheadRussell] p. 147Theorem *10.2219.26 1767
[WhiteheadRussell] p. 149Theorem *10.251pm10.251 37463
[WhiteheadRussell] p. 149Theorem *10.252pm10.252 37464
[WhiteheadRussell] p. 149Theorem *10.253pm10.253 37465
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1792
[WhiteheadRussell] p. 151Theorem *10.301albitr 37466
[WhiteheadRussell] p. 155Theorem *10.42pm10.42 37467
[WhiteheadRussell] p. 155Theorem *10.52pm10.52 37468
[WhiteheadRussell] p. 155Theorem *10.53pm10.53 37469
[WhiteheadRussell] p. 155Theorem *10.541pm10.541 37470
[WhiteheadRussell] p. 156Theorem *10.55pm10.55 37472
[WhiteheadRussell] p. 156Theorem *10.56pm10.56 37473
[WhiteheadRussell] p. 156Theorem *10.57pm10.57 37474
[WhiteheadRussell] p. 156Theorem *10.542pm10.542 37471
[WhiteheadRussell] p. 159Axiom *11.07pm11.07 2339
[WhiteheadRussell] p. 159Theorem *11.11pm11.11 37477
[WhiteheadRussell] p. 159Theorem *11.12pm11.12 37478
[WhiteheadRussell] p. 159Theorem PM*11.12stdpc4 2246
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1975
[WhiteheadRussell] p. 160Theorem *11.222exnaln 1734
[WhiteheadRussell] p. 160Theorem *11.252nexaln 1735
[WhiteheadRussell] p. 161Theorem *11.319.21vv 37479
[WhiteheadRussell] p. 162Theorem *11.322alim 37480
[WhiteheadRussell] p. 162Theorem *11.332albi 37481
[WhiteheadRussell] p. 162Theorem *11.342exim 37482
[WhiteheadRussell] p. 162Theorem *11.36spsbce-2 37484
[WhiteheadRussell] p. 162Theorem *11.3412exbi 37483
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1784
[WhiteheadRussell] p. 163Theorem *11.4319.36vv 37486
[WhiteheadRussell] p. 163Theorem *11.4419.31vv 37487
[WhiteheadRussell] p. 163Theorem *11.42119.33-2 37485
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1733
[WhiteheadRussell] p. 164Theorem *11.4619.37vv 37488
[WhiteheadRussell] p. 164Theorem *11.4719.28vv 37489
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1749
[WhiteheadRussell] p. 164Theorem *11.52pm11.52 37490
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 2122
[WhiteheadRussell] p. 164Theorem *11.5212exanali 37491
[WhiteheadRussell] p. 165Theorem *11.6pm11.6 37496
[WhiteheadRussell] p. 165Theorem *11.56aaanv 37492
[WhiteheadRussell] p. 165Theorem *11.57pm11.57 37493
[WhiteheadRussell] p. 165Theorem *11.58pm11.58 37494
[WhiteheadRussell] p. 165Theorem *11.59pm11.59 37495
[WhiteheadRussell] p. 166Theorem *11.7pm11.7 37500
[WhiteheadRussell] p. 166Theorem *11.61pm11.61 37497
[WhiteheadRussell] p. 166Theorem *11.62pm11.62 37498
[WhiteheadRussell] p. 166Theorem *11.63pm11.63 37499
[WhiteheadRussell] p. 166Theorem *11.71pm11.71 37501
[WhiteheadRussell] p. 175Definition *14.02df-eu 2366
[WhiteheadRussell] p. 178Theorem *13.13pm13.13a 37512  pm13.13b 37513
[WhiteheadRussell] p. 178Theorem *13.14pm13.14 37514
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2767
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2768
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 3217
[WhiteheadRussell] p. 179Theorem *13.212sbc6g 37520
[WhiteheadRussell] p. 179Theorem *13.222sbc5g 37521
[WhiteheadRussell] p. 179Theorem *13.192pm13.192 37515
[WhiteheadRussell] p. 179Theorem *13.1932pm13.193 37671  pm13.193 37516
[WhiteheadRussell] p. 179Theorem *13.194pm13.194 37517
[WhiteheadRussell] p. 179Theorem *13.195pm13.195 37518
[WhiteheadRussell] p. 179Theorem *13.196pm13.196a 37519
[WhiteheadRussell] p. 184Theorem *14.12pm14.12 37526
[WhiteheadRussell] p. 184Theorem *14.111iotasbc2 37525
[WhiteheadRussell] p. 184Definition *14.01iotasbc 37524
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3359
[WhiteheadRussell] p. 185Theorem *14.122pm14.122a 37527  pm14.122b 37528  pm14.122c 37529
[WhiteheadRussell] p. 185Theorem *14.123pm14.123a 37530  pm14.123b 37531  pm14.123c 37532
[WhiteheadRussell] p. 189Theorem *14.2iotaequ 37534
[WhiteheadRussell] p. 189Theorem *14.18pm14.18 37533
[WhiteheadRussell] p. 189Theorem *14.202iotavalb 37535
[WhiteheadRussell] p. 190Theorem *14.22iota4 5671
[WhiteheadRussell] p. 190Theorem *14.205iotasbc5 37536
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5672
[WhiteheadRussell] p. 191Theorem *14.24pm14.24 37537
[WhiteheadRussell] p. 192Theorem *14.25sbiota1 37539
[WhiteheadRussell] p. 192Theorem *14.26eupick 2428  eupickbi 2431  sbaniota 37540
[WhiteheadRussell] p. 192Theorem *14.242iotavalsb 37538
[WhiteheadRussell] p. 192Theorem *14.271eubi 37541
[WhiteheadRussell] p. 193Theorem *14.272iotasbcq 37542
[WhiteheadRussell] p. 235Definition *30.01conventions 26389  df-fv 5697
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 8584  pm54.43lem 8583
[Young] p. 141Definition of operator orderingleop2 28156
[Young] p. 142Example 12.2(i)0leop 28162  idleop 28163
[vandenDries] p. 42Lemma 61irrapx1 36285
[vandenDries] p. 43Theorem 62pellex 36292  pellexlem1 36286

This page was last updated on 18-Sep-2021.
Copyright terms: Public domain