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  Basic number theory
PART 12  GRAPH THEORY
      12.1  Vertices and edges
      12.2  Undirected graphs
      12.3  Walks, paths and cycles
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 BJ
      14.3  Mathbox for Jim Kingdon
      14.4  Mathbox for Mykola Mostovenko
      14.5  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 617
            1.2.6  Logical disjunction   wo 713
            1.2.7  Stable propositions   wstab 835
            1.2.8  Decidable propositions   wdc 839
            ​*1.2.9  Theorems of decidable propositions   const 857
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 921
            ​*1.2.11  The conditional operator for propositions   wif 983
            1.2.12  Abbreviated conjunction and disjunction of three wff's   w3o 1001
            1.2.13  True and false constants   wal 1393
                  ​*1.2.13.1  Universal quantifier for use by df-tru   wal 1393
                  ​*1.2.13.2  Equality predicate for use by df-tru   cv 1394
                  1.2.13.3  Define the true and false constants   wtru 1396
            1.2.14  Logical 'xor'   wxo 1417
            ​*1.2.15  Truth tables: Operations on true and false constants   truantru 1443
            ​*1.2.16  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1465
            1.2.17  Logical implication (continued)   syl6an 1476
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1493
            ​*1.3.2  Equality predicate (continued)   weq 1549
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1572
            1.3.4  Introduce Axiom of Existence   ax-i9 1576
            1.3.5  Additional intuitionistic axioms   ax-ial 1580
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1582
            1.3.7  The existential quantifier   19.8a 1636
            1.3.8  Equality theorems without distinct variables   a9e 1742
            1.3.9  Axioms ax-10 and ax-11   ax10o 1761
            1.3.10  Substitution (without distinct variables)   wsb 1808
            1.3.11  Theorems using axiom ax-11   equs5a 1840
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1857
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1868
            1.4.3  More theorems related to ax-11 and substitution   albidv 1870
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1904
            1.4.5  More substitution theorems   hbs1 1989
            1.4.6  Existential uniqueness   weu 2077
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2176
      ​​*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 2211
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2215
                  2.1.2.1  Elementary properties of class abstractions   eqabdv 2358
            2.1.3  Class form not-free predicate   wnfc 2359
            2.1.4  Negated equality and membership   wne 2400
                  2.1.4.1  Negated equality   wne 2400
                  2.1.4.2  Negated membership   wnel 2495
            2.1.5  Restricted quantification   wral 2508
            2.1.6  The universal class   cvv 2799
            ​*2.1.7  Conditional equality (experimental)   wcdeq 3011
            2.1.8  Russell's Paradox   ru 3027
            2.1.9  Proper substitution of classes for sets   wsbc 3028
            2.1.10  Proper substitution of classes for sets into classes   csb 3124
            2.1.11  Define basic set operations and relations   cdif 3194
            2.1.12  Subclasses and subsets   df-ss 3210
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3314
                  2.1.13.1  The difference of two classes   dfdif3 3314
                  2.1.13.2  The union of two classes   elun 3345
                  2.1.13.3  The intersection of two classes   elin 3387
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3435
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3470
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3484
            2.1.14  The empty set   c0 3491
            2.1.15  Conditional operator   cif 3602
            2.1.16  Power classes   cpw 3649
            2.1.17  Unordered and ordered pairs   csn 3666
            2.1.18  The union of a class   cuni 3888
            2.1.19  The intersection of a class   cint 3923
            2.1.20  Indexed union and intersection   ciun 3965
            2.1.21  Disjointness   wdisj 4059
            2.1.22  Binary relations   wbr 4083
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4144
            2.1.24  Transitive classes   wtr 4182
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4199
            2.2.2  Introduce the Axiom of Separation   ax-sep 4202
            2.2.3  Derive the Null Set Axiom   zfnuleu 4208
            2.2.4  Theorems requiring subset and intersection existence   nalset 4214
            2.2.5  Theorems requiring empty set existence   class2seteq 4248
            2.2.6  Collection principle   bnd 4257
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4259
            2.3.2  A notation for excluded middle   wem 4279
            2.3.3  Axiom of Pairing   ax-pr 4294
            2.3.4  Ordered pair theorem   opm 4321
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4345
            2.3.6  Power class of union and intersection   pwin 4374
            2.3.7  Epsilon and identity relations   cep 4379
            ​*2.3.8  Partial and total orderings   wpo 4386
            2.3.9  Founded and set-like relations   wfrfor 4419
            2.3.10  Ordinals   word 4454
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4525
            2.4.2  Ordinals (continued)   ordon 4579
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4625
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4630
            2.5.3  Transfinite induction   tfi 4675
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4681
            2.6.2  The natural numbers   com 4683
            2.6.3  Peano's postulates   peano1 4687
            2.6.4  Finite induction (for finite ordinals)   find 4692
            2.6.5  The Natural Numbers (continued)   nn0suc 4697
            2.6.6  Relations   cxp 4718
            2.6.7  Definite description binder (inverted iota)   cio 5279
            2.6.8  Functions   wfun 5315
            2.6.9  Cantor's Theorem   canth 5961
            2.6.10  Restricted iota (description binder)   crio 5962
            2.6.11  Operations   co 6010
            2.6.12  Maps-to notation   elmpocl 6209
            2.6.13  Function operation   cof 6225
            2.6.14  Functions (continued)   resfunexgALT 6262
            2.6.15  First and second members of an ordered pair   c1st 6293
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6395
            2.6.17  Function transposition   ctpos 6401
            2.6.18  Undefined values   pwuninel2 6439
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6441
            2.6.20  "Strong" transfinite recursion   crecs 6461
            2.6.21  Recursive definition generator   crdg 6526
            2.6.22  Finite recursion   cfrec 6547
            2.6.23  Ordinal arithmetic   c1o 6566
            2.6.24  Natural number arithmetic   nna0 6633
            2.6.25  Equivalence relations and classes   wer 6690
            2.6.26  The mapping operation   cmap 6808
            2.6.27  Infinite Cartesian products   cixp 6858
            2.6.28  Equinumerosity   cen 6898
            2.6.29  Equinumerosity (cont.)   xpf1o 7018
            2.6.30  Pigeonhole Principle   phplem1 7026
            2.6.31  Finite sets   fict 7043
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 7140
            2.6.33  Finite intersections   cfi 7151
            2.6.34  Supremum and infimum   csup 7165
            2.6.35  Ordinal isomorphism   ordiso2 7218
            2.6.36  Disjoint union   cdju 7220
                  2.6.36.1  Disjoint union   cdju 7220
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 7228
                  2.6.36.3  Universal property of the disjoint union   djuss 7253
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7276
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7285
                  2.6.36.6  Countable sets   0ct 7290
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7302
            2.6.38  Omniscient sets   comni 7317
            2.6.39  Markov's principle   cmarkov 7334
            2.6.40  Weakly omniscient sets   cwomni 7346
            2.6.41  Cardinal numbers   ccrd 7365
            2.6.42  Axiom of Choice equivalents   wac 7403
            2.6.43  Cardinal number arithmetic   endjudisj 7408
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7419
            2.6.45  Excluded middle and the power set of a singleton   iftrueb01 7424
            2.6.46  Apartness relations   wap 7449
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7464
​​*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 7475
            4.1.2  Final derivation of real and complex number postulates   axcnex 8062
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 8106
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 8139
            4.2.2  Infinity and the extended real number system   cpnf 8194
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 8229
            4.2.4  Ordering on reals   lttr 8236
            4.2.5  Initial properties of the complex numbers   mul12 8291
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8320
            4.3.2  Subtraction   cmin 8333
            4.3.3  Multiplication   kcnktkm1cn 8545
            4.3.4  Ordering on reals (cont.)   ltadd2 8582
            4.3.5  Real Apartness   creap 8737
            4.3.6  Complex Apartness   cap 8744
            4.3.7  Reciprocals   recextlem1 8814
            4.3.8  Division   cdiv 8835
            4.3.9  Ordering on reals (cont.)   ltp1 9007
            4.3.10  Suprema   lbreu 9108
            4.3.11  Imaginary and complex number properties   crap0 9121
            4.3.12  Function operation analogue theorems   ofnegsub 9125
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 9126
            4.4.2  Principle of mathematical induction   nnind 9142
            ​*4.4.3  Decimal representation of numbers   c2 9177
            ​*4.4.4  Some properties of specific numbers   neg1cn 9231
            4.4.5  Simple number properties   halfcl 9353
            4.4.6  The Archimedean property   arch 9382
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9385
            ​*4.4.8  Extended nonnegative integers   cxnn0 9448
            4.4.9  Integers (as a subset of complex numbers)   cz 9462
            4.4.10  Decimal arithmetic   cdc 9594
            4.4.11  Upper sets of integers   cuz 9738
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9831
            4.4.13  Complex numbers as pairs of reals   cnref1o 9863
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9866
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9982
            4.5.3  Real number intervals   cioo 10101
            4.5.4  Finite intervals of integers   cfz 10221
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10325
            4.5.6  Half-open integer ranges   cfzo 10355
            4.5.7  Rational numbers (cont.)   qtri3or 10477
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10505
            4.6.2  The modulo (remainder) operation   cmo 10561
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10638
            4.6.4  Strong induction over upper sets of integers   uzsinds 10683
            4.6.5  The infinite sequence builder "seq"   cseq 10686
            4.6.6  Integer powers   cexp 10777
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10958
            4.6.8  Factorial function   cfa 10964
            4.6.9  The binomial coefficient operation   cbc 10986
            4.6.10  The ` # ` (set size) function   chash 11014
                  4.6.10.1  Proper unordered pairs and triples (sets of size 2 and 3)   hash2en 11083
                  4.6.10.2  Functions with a domain containing at least two different elements   fundm2domnop0 11085
      ​​*4.7  Words over a set
            4.7.1  Definitions and basic theorems   cword 11089
            4.7.2  Last symbol of a word   clsw 11134
            4.7.3  Concatenations of words   cconcat 11143
            4.7.4  Singleton words   cs1 11168
            4.7.5  Concatenations with singleton words   ccatws1cl 11185
            4.7.6  Subwords/substrings   csubstr 11198
            4.7.7  Prefixes of a word   cpfx 11225
            4.7.8  Subwords of subwords   swrdswrdlem 11257
            4.7.9  Subwords and concatenations   pfxcctswrd 11263
            4.7.10  Subwords of concatenations   swrdccatfn 11277
            4.7.11  Longer string literals   cs2 11302
      ​4.8  Elementary real and complex functions
            4.8.1  The "shift" operation   cshi 11346
            4.8.2  Real and imaginary parts; conjugate   ccj 11371
            4.8.3  Sequence convergence   caucvgrelemrec 11511
            4.8.4  Square root; absolute value   csqrt 11528
            4.8.5  The maximum of two real numbers   maxcom 11735
            4.8.6  The minimum of two real numbers   mincom 11761
            4.8.7  The maximum of two extended reals   xrmaxleim 11776
            4.8.8  The minimum of two extended reals   xrnegiso 11794
      ​4.9  Elementary limits and convergence
            4.9.1  Limits   cli 11810
            4.9.2  Finite and infinite sums   csu 11885
            4.9.3  The binomial theorem   binomlem 12015
            4.9.4  Infinite sums (cont.)   isumshft 12022
            4.9.5  Miscellaneous converging and diverging sequences   divcnv 12029
            4.9.6  Arithmetic series   arisum 12030
            4.9.7  Geometric series   expcnvap0 12034
            4.9.8  Ratio test for infinite series convergence   cvgratnnlembern 12055
            4.9.9  Mertens' theorem   mertenslemub 12066
            4.9.10  Finite and infinite products   prodf 12070
                  4.9.10.1  Product sequences   prodf 12070
                  4.9.10.2  Non-trivial convergence   ntrivcvgap 12080
                  4.9.10.3  Complex products   cprod 12082
                  4.9.10.4  Finite products   fprodseq 12115
      ​4.10  Elementary trigonometry
            4.10.1  The exponential, sine, and cosine functions   ce 12174
                  4.10.1.1  The circle constant (tau = 2 pi)   ctau 12307
            4.10.2  _e is irrational   eirraplem 12309
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 12319
            ​*5.1.2  Even and odd numbers   evenelz 12399
            5.1.3  The division algorithm   divalglemnn 12450
            5.1.4  Bit sequences   cbits 12472
            5.1.5  The greatest common divisor operator   cgcd 12495
            5.1.6  Bézout's identity   bezoutlemnewy 12538
            5.1.7  Decidable sets of integers   nnmindc 12576
            5.1.8  Algorithms   nn0seqcvgd 12584
            5.1.9  Euclid's Algorithm   eucalgval2 12596
            ​*5.1.10  The least common multiple   clcm 12603
            ​*5.1.11  Coprimality and Euclid's lemma   coprmgcdb 12631
            5.1.12  Cancellability of congruences   congr 12643
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12650
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12687
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12704
            5.2.4  Properties of the canonical representation of a rational   cnumer 12724
            5.2.5  Euler's theorem   codz 12751
            5.2.6  Arithmetic modulo a prime number   modprm1div 12791
            5.2.7  Pythagorean Triples   coprimeprodsq 12801
            5.2.8  The prime count function   cpc 12828
            5.2.9  Pocklington's theorem   prmpwdvds 12899
            5.2.10  Infinite primes theorem   infpnlem1 12903
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 12907
            5.2.12  Lagrange's four-square theorem   cgz 12913
            5.2.13  Decimal arithmetic (cont.)   dec2dvds 12955
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12984
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 13049
            6.1.2  Slot definitions   cplusg 13131
            6.1.3  Definition of the structure product   crest 13293
            6.1.4  Definition of the structure quotient   cimas 13353
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 13407
            ​*7.1.2  Identity elements   mgmidmo 13426
            ​*7.1.3  Iterated sums in a magma   fngsum 13442
            ​*7.1.4  Semigroups   csgrp 13455
            ​*7.1.5  Definition and basic properties of monoids   cmnd 13470
            7.1.6  Monoid homomorphisms and submonoids   cmhm 13511
            ​*7.1.7  Iterated sums in a monoid   gsumvallem2 13547
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 13554
            ​*7.2.2  Group multiple operation   cmg 13677
            7.2.3  Subgroups and Quotient groups   csubg 13725
            7.2.4  Elementary theory of group homomorphisms   cghm 13798
            7.2.5  Abelian groups   ccmn 13842
                  7.2.5.1  Definition and basic properties   ccmn 13842
                  7.2.5.2  Group sum operation   gsumfzreidx 13895
      ​7.3  Rings
            7.3.1  Multiplicative Group   cmgp 13904
            ​*7.3.2  Non-unital rings ("rngs")   crng 13916
            ​*7.3.3  Ring unity (multiplicative identity)   cur 13943
            7.3.4  Semirings   csrg 13947
            7.3.5  Definition and basic properties of unital rings   crg 13980
            7.3.6  Opposite ring   coppr 14051
            7.3.7  Divisibility   cdsr 14070
            7.3.8  Ring homomorphisms   crh 14135
            7.3.9  Nonzero rings and zero rings   cnzr 14164
            7.3.10  Local rings   clring 14175
            7.3.11  Subrings   csubrng 14182
                  7.3.11.1  Subrings of non-unital rings   csubrng 14182
                  7.3.11.2  Subrings of unital rings   csubrg 14202
            7.3.12  Left regular elements and domains   crlreg 14240
      ​7.4  Division rings and fields
            7.4.1  Ring apartness   capr 14265
      ​7.5  Left modules
            7.5.1  Definition and basic properties   clmod 14272
            7.5.2  Subspaces and spans in a left module   clss 14337
      ​7.6  Subring algebras and ideals
            7.6.1  Subring algebras   csra 14418
            7.6.2  Ideals and spans   clidl 14452
            7.6.3  Two-sided ideals and quotient rings   c2idl 14484
            7.6.4  Principal ideal rings. Divisibility in the integers   rspsn 14519
      ​7.7  The complex numbers as an algebraic extensible structure
            7.7.1  Definition and basic properties   cpsmet 14520
            ​*7.7.2  Ring of integers   czring 14575
            7.7.3  Algebraic constructions based on the complex numbers   czrh 14596
​​*PART 8  BASIC LINEAR ALGEBRA
      ​8.1  Abstract multivariate polynomials
            8.1.1  Definition and basic properties   cmps 14646
​PART 9  BASIC TOPOLOGY
      ​9.1  Topology
            ​*9.1.1  Topological spaces   ctop 14692
                  9.1.1.1  Topologies   ctop 14692
                  9.1.1.2  Topologies on sets   ctopon 14705
                  9.1.1.3  Topological spaces   ctps 14725
            9.1.2  Topological bases   ctb 14737
            9.1.3  Examples of topologies   distop 14780
            9.1.4  Closure and interior   ccld 14787
            9.1.5  Neighborhoods   cnei 14833
            9.1.6  Subspace topologies   restrcl 14862
            9.1.7  Limits and continuity in topological spaces   ccn 14880
            9.1.8  Product topologies   ctx 14947
            9.1.9  Continuous function-builders   cnmptid 14976
            9.1.10  Homeomorphisms   chmeo 14995
      ​9.2  Metric spaces
            9.2.1  Pseudometric spaces   psmetrel 15017
            9.2.2  Basic metric space properties   cxms 15031
            9.2.3  Metric space balls   blfvalps 15080
            9.2.4  Open sets of a metric space   mopnrel 15136
            9.2.5  Continuity in metric spaces   metcnp3 15206
            9.2.6  Topology on the reals   qtopbasss 15216
            9.2.7  Topological definitions using the reals   ccncf 15265
​PART 10  BASIC REAL AND COMPLEX ANALYSIS
      ​10.1  Continuity
            10.1.1  Dedekind cuts   dedekindeulemuub 15312
            10.1.2  Intermediate value theorem   ivthinclemlm 15329
      ​10.2  Derivatives
            10.2.1  Real and complex differentiation   climc 15349
                  10.2.1.1  Derivatives of functions of one complex or real variable   climc 15349
​PART 11  BASIC REAL AND COMPLEX FUNCTIONS
      ​11.1  Polynomials
            11.1.1  Elementary properties of complex polynomials   cply 15423
      ​11.2  Basic trigonometry
            11.2.1  The exponential, sine, and cosine functions (cont.)   efcn 15463
            11.2.2  Properties of pi = 3.14159...   pilem1 15474
            11.2.3  The natural logarithm on complex numbers   clog 15551
            ​*11.2.4  Logarithms to an arbitrary base   clogb 15638
            11.2.5  Quartic binomial expansion   binom4 15674
      ​11.3  Basic number theory
            11.3.1  Wilson's theorem   wilthlem1 15675
            11.3.2  Number-theoretical functions   csgm 15676
            11.3.3  Perfect Number Theorem   mersenne 15692
            ​*11.3.4  Quadratic residues and the Legendre symbol   clgs 15697
            ​*11.3.5  Gauss' Lemma   gausslemma2dlem0a 15749
            11.3.6  Quadratic reciprocity   lgseisenlem1 15770
            11.3.7  All primes 4n+1 are the sum of two squares   2sqlem1 15814
​PART 12  GRAPH THEORY
      ​12.1  Vertices and edges
            12.1.1  The edge function extractor for extensible structures   cedgf 15826
            12.1.2  Vertices and indexed edges   cvtx 15834
                  12.1.2.1  Definitions and basic properties   cvtx 15834
                  12.1.2.2  The vertices and edges of a graph represented as ordered pair   opvtxval 15843
                  12.1.2.3  The vertices and edges of a graph represented as extensible structure   funvtxdm2domval 15851
                  12.1.2.4  Degenerated cases of representations of graphs   vtxval0 15875
            12.1.3  Edges as range of the edge function   cedg 15879
      ​12.2  Undirected graphs
            12.2.1  Undirected hypergraphs   cuhgr 15888
            12.2.2  Undirected pseudographs and multigraphs   cupgr 15912
            ​*12.2.3  Loop-free graphs   umgrislfupgrenlem 15949
            12.2.4  Edges as subsets of vertices of graphs   uhgredgiedgb 15953
            ​*12.2.5  Undirected simple graphs   cuspgr 15972
            12.2.6  Examples for graphs   usgr0e 16051
            12.2.7  Vertex degree   cvtxdg 16072
      ​12.3  Walks, paths and cycles
            12.3.1  Walks   cwlks 16089
            12.3.2  Trails   ctrls 16150
            12.3.3  Closed walks as words   cclwwlk 16160
                  12.3.3.1  Closed walks as words   cclwwlk 16160
                  12.3.3.2  Closed walks of a fixed length as words   cclwwlkn 16172
​PART 13  GUIDES AND MISCELLANEA
      ​13.1  Guides (conventions, explanations, and examples)
            ​*13.1.1  Conventions   conventions 16194
            13.1.2  Definitional examples   ex-or 16195
​PART 14  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​14.1  Mathboxes for user contributions
            14.1.1  Mathbox guidelines   mathbox 16205
      ​14.2  Mathbox for BJ
            14.2.1  Propositional calculus   bj-nnsn 16206
                  ​*14.2.1.1  Stable formulas   bj-trst 16212
                  14.2.1.2  Decidable formulas   bj-trdc 16225
            14.2.2  Predicate calculus   bj-ex 16235
            14.2.3  Set theorey miscellaneous   bj-el2oss1o 16247
            ​*14.2.4  Extensionality   bj-vtoclgft 16248
            ​*14.2.5  Decidability of classes   wdcin 16266
            14.2.6  Disjoint union   djucllem 16273
            14.2.7  Miscellaneous   funmptd 16276
            ​*14.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 16284
                  *14.2.8.1  Bounded formulas   wbd 16284
                  ​*14.2.8.2  Bounded classes   wbdc 16312
            ​*14.2.9  CZF: Bounded separation   ax-bdsep 16356
                  14.2.9.1  Delta_0-classical logic   ax-bj-d0cl 16396
                  14.2.9.2  Inductive classes and the class of natural number ordinals   wind 16398
                  ​*14.2.9.3  The first three Peano postulates   bj-peano2 16411
            ​*14.2.10  CZF: Infinity   ax-infvn 16413
                  *14.2.10.1  The set of natural number ordinals   ax-infvn 16413
                  ​*14.2.10.2  Peano's fifth postulate   bdpeano5 16415
                  ​*14.2.10.3  Bounded induction and Peano's fourth postulate   findset 16417
            ​*14.2.11  CZF: Set induction   setindft 16437
                  *14.2.11.1  Set induction   setindft 16437
                  ​*14.2.11.2  Full induction   bj-findis 16451
            ​*14.2.12  CZF: Strong collection   ax-strcoll 16454
            ​*14.2.13  CZF: Subset collection   ax-sscoll 16459
            14.2.14  Real numbers   ax-ddkcomp 16461
      ​14.3  Mathbox for Jim Kingdon
            14.3.1  Propositional and predicate logic   nnnotnotr 16462
            14.3.2  The sizes of sets   1dom1el 16463
            14.3.3  The power set of a singleton   pwtrufal 16476
            14.3.4  Omniscience of NN+oo   0nninf 16484
            14.3.5  Schroeder-Bernstein Theorem   exmidsbthrlem 16504
            14.3.6  Real and complex numbers   qdencn 16509
            ​*14.3.7  Analytic omniscience principles   trilpolemclim 16518
            14.3.8  Supremum and infimum   supfz 16553
            14.3.9  Circle constant   taupi 16555
      ​14.4  Mathbox for Mykola Mostovenko
      ​14.5  Mathbox for David A. Wheeler
            14.5.1  Testable propositions   dftest 16557
            ​*14.5.2  Allsome quantifier   walsi 16558