TOC of Theorem List - Intuitionistic Logic Explorer

Table of Contents Summary

PART 1  INTUITIONISTIC FIRST-ORDER LOGIC WITH EQUALITY
      1.1  Pre-logic
      1.2  Propositional calculus
      1.3  Predicate calculus mostly without distinct variables
      1.4  Predicate calculus with distinct variables
      1.5  First-order logic with one non-logical binary predicate
PART 2  SET THEORY
      2.1  IZF Set Theory - start with the Axiom of Extensionality
      2.2  IZF Set Theory - add the Axioms of Collection and Separation
      2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
      2.4  IZF Set Theory - add the Axiom of Union
      2.5  IZF Set Theory - add the Axiom of Set Induction
      2.6  IZF Set Theory - add the Axiom of Infinity
PART 3  CHOICE PRINCIPLES
      3.1  Countable Choice and Dependent Choice
PART 4  REAL AND COMPLEX NUMBERS
      4.1  Construction and axiomatization of real and complex numbers
      4.2  Derive the basic properties from the field axioms
      4.3  Real and complex numbers - basic operations
      4.4  Integer sets
      4.5  Order sets
      4.6  Elementary integer functions
      4.7  Words over a set
      4.8  Elementary real and complex functions
      4.9  Elementary limits and convergence
      4.10  Elementary trigonometry
PART 5  ELEMENTARY NUMBER THEORY
      5.1  Elementary properties of divisibility
      5.2  Elementary prime number theory
      5.3  Cardinality of real and complex number subsets
PART 6  BASIC STRUCTURES
      6.1  Extensible structures
PART 7  BASIC ALGEBRAIC STRUCTURES
      7.1  Monoids
      7.2  Groups
      7.3  Rings
      7.4  Division rings and fields
      7.5  Left modules
      7.6  Subring algebras and ideals
      7.7  The complex numbers as an algebraic extensible structure
PART 8  BASIC LINEAR ALGEBRA
      8.1  Abstract multivariate polynomials
PART 9  BASIC TOPOLOGY
      9.1  Topology
      9.2  Metric spaces
PART 10  BASIC REAL AND COMPLEX ANALYSIS
      10.1  Continuity
      10.2  Derivatives
PART 11  BASIC REAL AND COMPLEX FUNCTIONS
      11.1  Polynomials
      11.2  Basic trigonometry
      11.3  Pell equations
      11.4  Basic number theory
PART 12  GRAPH THEORY
      12.1  Vertices and edges
      12.2  Undirected graphs
      12.3  Walks, paths and cycles
      12.4  Eulerian paths and the Konigsberg Bridge problem
PART 13  GUIDES AND MISCELLANEA
      13.1  Guides (conventions, explanations, and examples)
PART 14  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​14.1  Mathboxes for user contributions
      14.2  Mathbox for Matthew House
      14.3  Mathbox for BJ
      14.4  Mathbox for Jim Kingdon
      14.5  Mathbox for Mykola Mostovenko
      14.6  Mathbox for David A. Wheeler

Detailed Table of Contents
(* means the section header has a description)

​​*PART 1  INTUITIONISTIC FIRST-ORDER LOGIC WITH EQUALITY
      ​*1.1  Pre-logic
            *1.1.1  Inferences for assisting proof development   idi 1
      ​​*1.2  Propositional calculus
            1.2.1  Recursively define primitive wffs for propositional calculus   wn 3
            1.2.2  Propositional logic axioms for implication   ax-mp 5
            ​*1.2.3  Logical implication   mp2b 8
            1.2.4  Logical conjunction and logical equivalence   wa 104
            1.2.5  Logical negation (intuitionistic)   ax-in1 619
            1.2.6  Logical disjunction   wo 716
            1.2.7  Stable propositions   wstab 838
            1.2.8  Decidable propositions   wdc 842
            ​*1.2.9  Theorems of decidable propositions   const 860
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 924
            ​*1.2.11  The conditional operator for propositions   wif 986
            1.2.12  Abbreviated conjunction and disjunction of three wff's   w3o 1004
            1.2.13  True and false constants   wal 1396
                  ​*1.2.13.1  Universal quantifier for use by df-tru   wal 1396
                  ​*1.2.13.2  Equality predicate for use by df-tru   cv 1397
                  1.2.13.3  Define the true and false constants   wtru 1399
            1.2.14  Logical 'xor'   wxo 1420
            ​*1.2.15  Truth tables: Operations on true and false constants   truantru 1446
            ​*1.2.16  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1468
            1.2.17  Logical implication (continued)   syl6an 1479
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1496
            ​*1.3.2  Equality predicate (continued)   weq 1552
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1575
            1.3.4  Introduce Axiom of Existence   ax-i9 1579
            1.3.5  Additional intuitionistic axioms   ax-ial 1583
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1585
            1.3.7  The existential quantifier   19.8a 1639
            1.3.8  Equality theorems without distinct variables   a9e 1744
            1.3.9  Axioms ax-10 and ax-11   ax10o 1763
            1.3.10  Substitution (without distinct variables)   wsb 1811
            1.3.11  Theorems using axiom ax-11   equs5a 1843
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1860
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1871
            1.4.3  More theorems related to ax-11 and substitution   albidv 1873
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1907
            1.4.5  More substitution theorems   hbs1 1994
            1.4.6  Existential uniqueness   weu 2082
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2181
      ​​*1.5  First-order logic with one non-logical binary predicate
​​*PART 2  SET THEORY
      ​2.1  IZF Set Theory - start with the Axiom of Extensionality
            2.1.1  Introduce the Axiom of Extensionality   ax-ext 2216
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2220
                  2.1.2.1  Elementary properties of class abstractions   eqabdv 2365
            2.1.3  Class form not-free predicate   wnfc 2373
            2.1.4  Negated equality and membership   wne 2414
                  2.1.4.1  Negated equality   wne 2414
                  2.1.4.2  Negated membership   wnel 2509
            2.1.5  Restricted quantification   wral 2522
            2.1.6  The universal class   cvv 2815
            ​*2.1.7  Conditional equality (experimental)   wcdeq 3027
            2.1.8  Russell's Paradox   ru 3043
            2.1.9  Proper substitution of classes for sets   wsbc 3044
            2.1.10  Proper substitution of classes for sets into classes   csb 3140
            2.1.11  Define basic set operations and relations   cdif 3210
            2.1.12  Subclasses and subsets   df-ss 3226
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3331
                  2.1.13.1  The difference of two classes   dfdif3 3331
                  2.1.13.2  The union of two classes   elun 3362
                  2.1.13.3  The intersection of two classes   elin 3404
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3454
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3489
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3503
            2.1.14  The empty set   c0 3510
            2.1.15  Conditional operator   cif 3622
            2.1.16  Power classes   cpw 3671
            2.1.17  Unordered and ordered pairs   csn 3691
            2.1.18  The union of a class   cuni 3916
            2.1.19  The intersection of a class   cint 3951
            2.1.20  Indexed union and intersection   ciun 3993
            2.1.21  Disjointness   wdisj 4087
            2.1.22  Binary relations   wbr 4111
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4172
            2.1.24  Transitive classes   wtr 4210
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4227
            2.2.2  Introduce the Axiom of Separation   ax-sep 4230
            2.2.3  Derive the Null Set Axiom   zfnuleu 4236
            2.2.4  Theorems requiring subset and intersection existence   nalset 4242
            2.2.5  Theorems requiring empty set existence   class2seteq 4278
            2.2.6  Collection principle   bnd 4287
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4289
            2.3.2  A notation for excluded middle   wem 4309
            2.3.3  Axiom of Pairing   ax-pr 4324
            2.3.4  Ordered pair theorem   opm 4352
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4376
            2.3.6  Power class of union and intersection   pwin 4405
            2.3.7  Epsilon and identity relations   cep 4410
            ​*2.3.8  Partial and total orderings   wpo 4417
            2.3.9  Founded and set-like relations   wfrfor 4450
            2.3.10  Ordinals   word 4485
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4556
            2.4.2  Ordinals (continued)   ordon 4610
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4656
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4661
            2.5.3  Transfinite induction   tfi 4706
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4712
            2.6.2  The natural numbers   com 4714
            2.6.3  Peano's postulates   peano1 4718
            2.6.4  Finite induction (for finite ordinals)   find 4723
            2.6.5  The Natural Numbers (continued)   nn0suc 4728
            2.6.6  Relations   cxp 4749
            2.6.7  Definite description binder (inverted iota)   cio 5312
            2.6.8  Functions   wfun 5348
            2.6.9  Cantor's Theorem   canth 6003
            2.6.10  Restricted iota (description binder)   crio 6004
            2.6.11  Operations   co 6052
            2.6.12  Maps-to notation   elmpocl 6251
            2.6.13  Function operation   cof 6266
            2.6.14  Functions (continued)   resfunexgALT 6303
            2.6.15  First and second members of an ordered pair   c1st 6334
            ​*2.6.16  The support of functions   csupp 6437
            ​*2.6.17  Special maps-to operations   opeliunxp2f 6471
            2.6.18  Function transposition   ctpos 6477
            2.6.19  Undefined values   pwuninel2 6515
            2.6.20  Functions on ordinals; strictly monotone ordinal functions   iunon 6517
            2.6.21  "Strong" transfinite recursion   crecs 6537
            2.6.22  Recursive definition generator   crdg 6602
            2.6.23  Finite recursion   cfrec 6623
            2.6.24  Ordinal arithmetic   c1o 6642
            2.6.25  Natural number arithmetic   nna0 6709
            2.6.26  Equivalence relations and classes   wer 6766
            2.6.27  The mapping operation   cmap 6884
            2.6.28  Infinite Cartesian products   cixp 6935
            2.6.29  Equinumerosity   cen 6975
            2.6.30  Equinumerosity (cont.)   xpf1o 7099
            2.6.31  Pigeonhole Principle   phplem1 7108
            2.6.32  Finite sets   fict 7125
            2.6.33  Schroeder-Bernstein Theorem   sbthlem1 7229
            2.6.34  Finitely supported functions   cfsupp 7240
            2.6.35  Finite intersections   cfi 7257
            2.6.36  The sizes of sets   2omap 7271
            2.6.37  Supremum and infimum   csup 7275
            2.6.38  Ordinal isomorphism   ordiso2 7328
            2.6.39  Disjoint union   cdju 7330
                  2.6.39.1  Disjoint union   cdju 7330
                  ​*2.6.39.2  Left and right injections of a disjoint union   cinl 7338
                  2.6.39.3  Universal property of the disjoint union   djuss 7363
                  2.6.39.4  Dominance and equinumerosity properties of disjoint union   djudom 7386
                  2.6.39.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7395
                  2.6.39.6  Countable sets   0ct 7400
            ​*2.6.40  The one-point compactification of the natural numbers   xnninf 7412
            2.6.41  Omniscient sets   comni 7427
            2.6.42  Markov's principle   cmarkov 7444
            2.6.43  Weakly omniscient sets   cwomni 7456
            2.6.44  Cardinal numbers   ccrd 7475
            2.6.45  Axiom of Choice equivalents   wac 7514
            2.6.46  Cardinal number arithmetic   endjudisj 7519
            2.6.47  Ordinal trichotomy   exmidontriimlem1 7530
            2.6.48  Excluded middle and the power set of a singleton   iftrueb01 7535
            2.6.49  Apartness relations   wap 7560
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7578
​​*PART 4  REAL AND COMPLEX NUMBERS
      ​4.1  Construction and axiomatization of real and complex numbers
            4.1.1  Dedekind-cut construction of real and complex numbers   cnpi 7589
            4.1.2  Final derivation of real and complex number postulates   axcnex 8176
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 8220
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 8253
            4.2.2  Infinity and the extended real number system   cpnf 8307
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 8342
            4.2.4  Ordering on reals   lttr 8349
            4.2.5  Initial properties of the complex numbers   mul12 8404
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8433
            4.3.2  Subtraction   cmin 8446
            4.3.3  Multiplication   kcnktkm1cn 8658
            4.3.4  Ordering on reals (cont.)   ltadd2 8695
            4.3.5  Real Apartness   creap 8850
            4.3.6  Complex Apartness   cap 8857
            4.3.7  Reciprocals   recextlem1 8927
            4.3.8  Division   cdiv 8948
            4.3.9  Ordering on reals (cont.)   ltp1 9120
            4.3.10  Suprema   lbreu 9221
            4.3.11  Imaginary and complex number properties   crap0 9234
            4.3.12  Function operation analogue theorems   ofnegsub 9238
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 9239
            4.4.2  Principle of mathematical induction   nnind 9255
            ​*4.4.3  Decimal representation of numbers   c2 9290
            ​*4.4.4  Some properties of specific numbers   neg1cn 9344
            4.4.5  Simple number properties   halfcl 9466
            4.4.6  The Archimedean property   arch 9495
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9498
            ​*4.4.8  Extended nonnegative integers   cxnn0 9565
            4.4.9  Integers (as a subset of complex numbers)   cz 9579
            4.4.10  Decimal arithmetic   cdc 9712
            4.4.11  Upper sets of integers   cuz 9856
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9954
            4.4.13  Complex numbers as pairs of reals   cnref1o 9986
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9989
            4.5.2  Infinity and the extended real number system (cont.)   cxne 10105
            4.5.3  Real number intervals   cioo 10224
            4.5.4  Finite intervals of integers   cfz 10345
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10450
            4.5.6  Half-open integer ranges   cfzo 10480
            4.5.7  Rational numbers (cont.)   qtri3or 10604
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10632
            4.6.2  The modulo (remainder) operation   cmo 10688
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10765
            4.6.4  Strong induction over upper sets of integers   uzsinds 10810
            4.6.5  The infinite sequence builder "seq"   cseq 10813
            4.6.6  Integer powers   cexp 10904
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 11085
            4.6.8  Factorial function   cfa 11091
            4.6.9  The binomial coefficient operation   cbc 11113
            4.6.10  The ` # ` (set size) function   chash 11142
                  4.6.10.1  Proper unordered pairs and triples (sets of size 2 and 3)   hash2en 11219
                  4.6.10.2  Functions with a domain containing at least two different elements   fundm2domnop0 11224
      ​​*4.7  Words over a set
            4.7.1  Definitions and basic theorems   cword 11228
            4.7.2  Last symbol of a word   clsw 11273
            4.7.3  Concatenations of words   cconcat 11282
            4.7.4  Singleton words   cs1 11307
            4.7.5  Concatenations with singleton words   ccatws1cl 11324
            4.7.6  Subwords/substrings   csubstr 11341
            4.7.7  Prefixes of a word   cpfx 11368
            4.7.8  Subwords of subwords   swrdswrdlem 11400
            4.7.9  Subwords and concatenations   pfxcctswrd 11406
            4.7.10  Subwords of concatenations   swrdccatfn 11420
            4.7.11  Longer string literals   cs2 11445
      ​4.8  Elementary real and complex functions
            4.8.1  The "shift" operation   cshi 11503
            4.8.2  Real and imaginary parts; conjugate   ccj 11528
            4.8.3  Sequence convergence   caucvgrelemrec 11668
            4.8.4  Square root; absolute value   csqrt 11685
            4.8.5  The maximum of two real numbers   maxcom 11892
            4.8.6  The minimum of two real numbers   mincom 11918
            4.8.7  The maximum of two extended reals   xrmaxleim 11933
            4.8.8  The minimum of two extended reals   xrnegiso 11951
      ​4.9  Elementary limits and convergence
            4.9.1  Limits   cli 11967
            4.9.2  Finite and infinite sums   csu 12042
            4.9.3  The binomial theorem   binomlem 12173
            4.9.4  Infinite sums (cont.)   isumshft 12180
            4.9.5  Miscellaneous converging and diverging sequences   divcnv 12187
            4.9.6  Arithmetic series   arisum 12188
            4.9.7  Geometric series   expcnvap0 12192
            4.9.8  Ratio test for infinite series convergence   cvgratnnlembern 12213
            4.9.9  Mertens' theorem   mertenslemub 12224
            4.9.10  Finite and infinite products   prodf 12228
                  4.9.10.1  Product sequences   prodf 12228
                  4.9.10.2  Non-trivial convergence   ntrivcvgap 12238
                  4.9.10.3  Complex products   cprod 12240
                  4.9.10.4  Finite products   fprodseq 12273
      ​4.10  Elementary trigonometry
            4.10.1  The exponential, sine, and cosine functions   ce 12332
                  4.10.1.1  The circle constant (tau = 2 pi)   ctau 12465
            4.10.2  _e is irrational   eirraplem 12467
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 12477
            ​*5.1.2  Even and odd numbers   evenelz 12557
            5.1.3  The division algorithm   divalglemnn 12608
            5.1.4  Bit sequences   cbits 12630
            5.1.5  The greatest common divisor operator   cgcd 12653
            5.1.6  Bézout's identity   bezoutlemnewy 12696
            5.1.7  Decidable sets of integers   nnmindc 12734
            5.1.8  Algorithms   nn0seqcvgd 12742
            5.1.9  Euclid's Algorithm   eucalgval2 12754
            ​*5.1.10  The least common multiple   clcm 12761
            ​*5.1.11  Coprimality and Euclid's lemma   coprmgcdb 12789
            5.1.12  Cancellability of congruences   congr 12801
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12808
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12845
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12862
            5.2.4  Properties of the canonical representation of a rational   cnumer 12882
            5.2.5  Euler's theorem   codz 12909
            5.2.6  Arithmetic modulo a prime number   modprm1div 12949
            5.2.7  Pythagorean Triples   coprimeprodsq 12959
            5.2.8  The prime count function   cpc 12986
            5.2.9  Pocklington's theorem   prmpwdvds 13057
            5.2.10  Infinite primes theorem   infpnlem1 13061
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 13065
            5.2.12  Lagrange's four-square theorem   cgz 13071
            5.2.13  Decimal arithmetic (cont.)   dec2dvds 13113
            5.2.14  Bertrand's Ballot Problem   ballotfilemofi 13142
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 13160
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 13225
            6.1.2  Slot definitions   cplusg 13307
            6.1.3  Definition of the structure product   crest 13469
            6.1.4  Definition of the structure quotient   cimas 13529
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 13583
            ​*7.1.2  Identity elements   mgmidmo 13602
            ​*7.1.3  Iterated sums in a magma   fngsum 13618
            ​*7.1.4  Semigroups   csgrp 13631
            ​*7.1.5  Definition and basic properties of monoids   cmnd 13646
            7.1.6  Monoid homomorphisms and submonoids   cmhm 13687
            ​*7.1.7  Iterated sums in a monoid   gsumvallem2 13723
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 13730
            ​*7.2.2  Group multiple operation   cmg 13853
            7.2.3  Subgroups and Quotient groups   csubg 13901
            7.2.4  Elementary theory of group homomorphisms   cghm 13974
            7.2.5  Abelian groups   ccmn 14018
                  7.2.5.1  Definition and basic properties   ccmn 14018
                  7.2.5.2  Group sum operation   gsumfzreidx 14071
      ​7.3  Rings
            7.3.1  Multiplicative Group   cmgp 14081
            ​*7.3.2  Non-unital rings ("rngs")   crng 14093
            ​*7.3.3  Ring unity (multiplicative identity)   cur 14120
            7.3.4  Semirings   csrg 14124
            7.3.5  Definition and basic properties of unital rings   crg 14157
            7.3.6  Opposite ring   coppr 14228
            7.3.7  Divisibility   cdsr 14247
            7.3.8  Ring homomorphisms   crh 14312
            7.3.9  Nonzero rings and zero rings   cnzr 14341
            7.3.10  Local rings   clring 14352
            7.3.11  Subrings   csubrng 14359
                  7.3.11.1  Subrings of non-unital rings   csubrng 14359
                  7.3.11.2  Subrings of unital rings   csubrg 14379
            7.3.12  Left regular elements and domains   crlreg 14417
      ​7.4  Division rings and fields
            7.4.1  Ring apartness   capr 14443
      ​7.5  Left modules
            7.5.1  Definition and basic properties   clmod 14452
            7.5.2  Subspaces and spans in a left module   clss 14517
      ​7.6  Subring algebras and ideals
            7.6.1  Subring algebras   csra 14598
            7.6.2  Ideals and spans   clidl 14632
            7.6.3  Two-sided ideals and quotient rings   c2idl 14664
            7.6.4  Principal ideal rings. Divisibility in the integers   rspsn 14699
      ​7.7  The complex numbers as an algebraic extensible structure
            7.7.1  Definition and basic properties   cpsmet 14700
            ​*7.7.2  Ring of integers   czring 14755
            7.7.3  Algebraic constructions based on the complex numbers   czrh 14776
​​*PART 8  BASIC LINEAR ALGEBRA
      ​8.1  Abstract multivariate polynomials
            8.1.1  Definition and basic properties   cmps 14826
​PART 9  BASIC TOPOLOGY
      ​9.1  Topology
            ​*9.1.1  Topological spaces   ctop 14879
                  9.1.1.1  Topologies   ctop 14879
                  9.1.1.2  Topologies on sets   ctopon 14892
                  9.1.1.3  Topological spaces   ctps 14912
            9.1.2  Topological bases   ctb 14924
            9.1.3  Examples of topologies   distop 14967
            9.1.4  Closure and interior   ccld 14974
            9.1.5  Neighborhoods   cnei 15020
            9.1.6  Subspace topologies   restrcl 15049
            9.1.7  Limits and continuity in topological spaces   ccn 15067
            9.1.8  Product topologies   ctx 15134
            9.1.9  Continuous function-builders   cnmptid 15163
            9.1.10  Homeomorphisms   chmeo 15182
      ​9.2  Metric spaces
            9.2.1  Pseudometric spaces   psmetrel 15204
            9.2.2  Basic metric space properties   cxms 15218
            9.2.3  Metric space balls   blfvalps 15267
            9.2.4  Open sets of a metric space   mopnrel 15323
            9.2.5  Continuity in metric spaces   metcnp3 15393
            9.2.6  Topology on the reals   qtopbasss 15403
            9.2.7  Topological definitions using the reals   ccncf 15452
​PART 10  BASIC REAL AND COMPLEX ANALYSIS
      ​10.1  Continuity
            10.1.1  Dedekind cuts   dedekindeulemuub 15499
            10.1.2  Intermediate value theorem   ivthinclemlm 15516
      ​10.2  Derivatives
            10.2.1  Real and complex differentiation   climc 15536
                  10.2.1.1  Derivatives of functions of one complex or real variable   climc 15536
​PART 11  BASIC REAL AND COMPLEX FUNCTIONS
      ​11.1  Polynomials
            11.1.1  Elementary properties of complex polynomials   cply 15610
      ​11.2  Basic trigonometry
            11.2.1  The exponential, sine, and cosine functions (cont.)   efcn 15650
            11.2.2  Properties of pi = 3.14159...   pilem1 15661
            11.2.3  The natural logarithm on complex numbers   clog 15738
            ​*11.2.4  Logarithms to an arbitrary base   clogb 15825
            11.2.5  Quartic binomial expansion   binom4 15861
      ​11.3  Pell equations
            11.3.1  Pell equations 1: A nontrivial solution always exists   pellexlem1 15862
      ​11.4  Basic number theory
            11.4.1  Wilson's theorem   wilthlem1 15865
            11.4.2  Number-theoretical functions   csgm 15866
            11.4.3  Perfect Number Theorem   mersenne 15882
            ​*11.4.4  Quadratic residues and the Legendre symbol   clgs 15887
            ​*11.4.5  Gauss' Lemma   gausslemma2dlem0a 15939
            11.4.6  Quadratic reciprocity   lgseisenlem1 15960
            11.4.7  All primes 4n+1 are the sum of two squares   2sqlem1 16004
​PART 12  GRAPH THEORY
      ​12.1  Vertices and edges
            12.1.1  The edge function extractor for extensible structures   cedgf 16016
            12.1.2  Vertices and indexed edges   cvtx 16024
                  12.1.2.1  Definitions and basic properties   cvtx 16024
                  12.1.2.2  The vertices and edges of a graph represented as ordered pair   opvtxval 16033
                  12.1.2.3  The vertices and edges of a graph represented as extensible structure   funvtxdm2domval 16041
                  12.1.2.4  Degenerated cases of representations of graphs   vtxval0 16065
            12.1.3  Edges as range of the edge function   cedg 16069
      ​12.2  Undirected graphs
            12.2.1  Undirected hypergraphs   cuhgr 16079
            12.2.2  Undirected pseudographs and multigraphs   cupgr 16103
            ​*12.2.3  Loop-free graphs   umgrislfupgrenlem 16142
            12.2.4  Edges as subsets of vertices of graphs   uhgredgiedgb 16146
            ​*12.2.5  Undirected simple graphs   cuspgr 16165
            12.2.6  Examples for graphs   usgr0e 16244
            12.2.7  Subgraphs   csubgr 16265
            12.2.8  Vertex degree   cvtxdg 16298
      ​12.3  Walks, paths and cycles
            12.3.1  Walks   cwlks 16329
            12.3.2  Trails   ctrls 16392
            12.3.3  Closed walks as words   cclwwlk 16403
                  12.3.3.1  Closed walks as words   cclwwlk 16403
                  12.3.3.2  Closed walks of a fixed length as words   cclwwlkn 16415
                  12.3.3.3  Closed walks on a vertex of a fixed length as words   cclwwlknon 16438
      ​12.4  Eulerian paths and the Konigsberg Bridge problem
            ​*12.4.1  Eulerian paths   ceupth 16454
            ​*12.4.2  The Königsberg Bridge problem   konigsbergvtx 16494
​PART 13  GUIDES AND MISCELLANEA
      ​13.1  Guides (conventions, explanations, and examples)
            ​*13.1.1  Conventions   conventions 16506
            13.1.2  Definitional examples   ex-or 16507
​PART 14  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​14.1  Mathboxes for user contributions
            14.1.1  Mathbox guidelines   mathbox 16517
      ​14.2  Mathbox for Matthew House
      ​14.3  Mathbox for BJ
            14.3.1  Propositional calculus   bj-nnsn 16522
                  ​*14.3.1.1  Stable formulas   bj-trst 16528
                  14.3.1.2  Decidable formulas   bj-trdc 16541
            14.3.2  Predicate calculus   bj-ex 16551
            14.3.3  Set theorey miscellaneous   bj-el2oss1o 16563
            ​*14.3.4  Extensionality   bj-vtoclgft 16564
            ​*14.3.5  Decidability of classes   wdcin 16582
            14.3.6  Disjoint union   djucllem 16589
            14.3.7  Miscellaneous   funmptd 16592
            ​*14.3.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 16599
                  *14.3.8.1  Bounded formulas   wbd 16599
                  ​*14.3.8.2  Bounded classes   wbdc 16627
            ​*14.3.9  CZF: Bounded separation   ax-bdsep 16671
                  14.3.9.1  Delta_0-classical logic   ax-bj-d0cl 16711
                  14.3.9.2  Inductive classes and the class of natural number ordinals   wind 16713
                  ​*14.3.9.3  The first three Peano postulates   bj-peano2 16726
            ​*14.3.10  CZF: Infinity   ax-infvn 16728
                  *14.3.10.1  The set of natural number ordinals   ax-infvn 16728
                  ​*14.3.10.2  Peano's fifth postulate   bdpeano5 16730
                  ​*14.3.10.3  Bounded induction and Peano's fourth postulate   findset 16732
            ​*14.3.11  CZF: Set induction   setindft 16752
                  *14.3.11.1  Set induction   setindft 16752
                  ​*14.3.11.2  Full induction   bj-findis 16766
            ​*14.3.12  CZF: Strong collection   ax-strcoll 16769
            ​*14.3.13  CZF: Subset collection   ax-sscoll 16774
            14.3.14  Real numbers   ax-ddkcomp 16776
      ​14.4  Mathbox for Jim Kingdon
            14.4.1  Propositional and predicate logic   nnnotnotr 16777
            14.4.2  The sizes of sets   ss1oel2o 16778
            14.4.3  The power set of a singleton   pwtrufal 16788
            14.4.4  Omniscience of NN+oo   0nninf 16799
            14.4.5  Schroeder-Bernstein Theorem   exmidsbthrlem 16819
            14.4.6  Real and complex numbers   qdencn 16824
            ​*14.4.7  Analytic omniscience principles   trilpolemclim 16837
            14.4.8  Supremum and infimum   supfz 16874
            14.4.9  Circle constant   taupi 16876
            14.4.10  Finite group sum over unordered finite set   cgfsu 16877
      ​14.5  Mathbox for Mykola Mostovenko
      ​14.6  Mathbox for David A. Wheeler
            14.6.1  Testable propositions   dftest 16889
            ​*14.6.2  Allsome quantifier   walsi 16890