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
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 712
            1.2.7  Stable propositions   wstab 834
            1.2.8  Decidable propositions   wdc 838
            ​*1.2.9  Theorems of decidable propositions   const 856
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 920
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 982
            1.2.12  True and false constants   wal 1373
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1373
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1374
                  1.2.12.3  Define the true and false constants   wtru 1376
            1.2.13  Logical 'xor'   wxo 1397
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1423
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1445
            1.2.16  Logical implication (continued)   syl6an 1456
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1473
            ​*1.3.2  Equality predicate (continued)   weq 1529
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1552
            1.3.4  Introduce Axiom of Existence   ax-i9 1556
            1.3.5  Additional intuitionistic axioms   ax-ial 1560
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1562
            1.3.7  The existential quantifier   19.8a 1616
            1.3.8  Equality theorems without distinct variables   a9e 1722
            1.3.9  Axioms ax-10 and ax-11   ax10o 1741
            1.3.10  Substitution (without distinct variables)   wsb 1788
            1.3.11  Theorems using axiom ax-11   equs5a 1820
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1837
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1848
            1.4.3  More theorems related to ax-11 and substitution   albidv 1850
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1884
            1.4.5  More substitution theorems   hbs1 1969
            1.4.6  Existential uniqueness   weu 2057
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2156
      ​​*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 2191
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2195
                  2.1.2.1  Elementary properties of class abstractions   eqabdv 2338
            2.1.3  Class form not-free predicate   wnfc 2339
            2.1.4  Negated equality and membership   wne 2380
                  2.1.4.1  Negated equality   wne 2380
                  2.1.4.2  Negated membership   wnel 2475
            2.1.5  Restricted quantification   wral 2488
            2.1.6  The universal class   cvv 2779
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2991
            2.1.8  Russell's Paradox   ru 3007
            2.1.9  Proper substitution of classes for sets   wsbc 3008
            2.1.10  Proper substitution of classes for sets into classes   csb 3104
            2.1.11  Define basic set operations and relations   cdif 3174
            2.1.12  Subclasses and subsets   df-ss 3190
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3294
                  2.1.13.1  The difference of two classes   dfdif3 3294
                  2.1.13.2  The union of two classes   elun 3325
                  2.1.13.3  The intersection of two classes   elin 3367
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3415
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3450
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3464
            2.1.14  The empty set   c0 3471
            2.1.15  Conditional operator   cif 3582
            2.1.16  Power classes   cpw 3629
            2.1.17  Unordered and ordered pairs   csn 3646
            2.1.18  The union of a class   cuni 3867
            2.1.19  The intersection of a class   cint 3902
            2.1.20  Indexed union and intersection   ciun 3944
            2.1.21  Disjointness   wdisj 4038
            2.1.22  Binary relations   wbr 4062
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4123
            2.1.24  Transitive classes   wtr 4161
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4178
            2.2.2  Introduce the Axiom of Separation   ax-sep 4181
            2.2.3  Derive the Null Set Axiom   zfnuleu 4187
            2.2.4  Theorems requiring subset and intersection existence   nalset 4193
            2.2.5  Theorems requiring empty set existence   class2seteq 4226
            2.2.6  Collection principle   bnd 4235
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4237
            2.3.2  A notation for excluded middle   wem 4257
            2.3.3  Axiom of Pairing   ax-pr 4272
            2.3.4  Ordered pair theorem   opm 4299
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4323
            2.3.6  Power class of union and intersection   pwin 4350
            2.3.7  Epsilon and identity relations   cep 4355
            ​*2.3.8  Partial and total orderings   wpo 4362
            2.3.9  Founded and set-like relations   wfrfor 4395
            2.3.10  Ordinals   word 4430
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4501
            2.4.2  Ordinals (continued)   ordon 4555
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4601
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4606
            2.5.3  Transfinite induction   tfi 4651
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4657
            2.6.2  The natural numbers   com 4659
            2.6.3  Peano's postulates   peano1 4663
            2.6.4  Finite induction (for finite ordinals)   find 4668
            2.6.5  The Natural Numbers (continued)   nn0suc 4673
            2.6.6  Relations   cxp 4694
            2.6.7  Definite description binder (inverted iota)   cio 5252
            2.6.8  Functions   wfun 5288
            2.6.9  Cantor's Theorem   canth 5925
            2.6.10  Restricted iota (description binder)   crio 5926
            2.6.11  Operations   co 5974
            2.6.12  Maps-to notation   elmpocl 6171
            2.6.13  Function operation   cof 6186
            2.6.14  Functions (continued)   resfunexgALT 6223
            2.6.15  First and second members of an ordered pair   c1st 6254
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6354
            2.6.17  Function transposition   ctpos 6360
            2.6.18  Undefined values   pwuninel2 6398
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6400
            2.6.20  "Strong" transfinite recursion   crecs 6420
            2.6.21  Recursive definition generator   crdg 6485
            2.6.22  Finite recursion   cfrec 6506
            2.6.23  Ordinal arithmetic   c1o 6525
            2.6.24  Natural number arithmetic   nna0 6590
            2.6.25  Equivalence relations and classes   wer 6647
            2.6.26  The mapping operation   cmap 6765
            2.6.27  Infinite Cartesian products   cixp 6815
            2.6.28  Equinumerosity   cen 6855
            2.6.29  Equinumerosity (cont.)   xpf1o 6973
            2.6.30  Pigeonhole Principle   phplem1 6981
            2.6.31  Finite sets   fict 6998
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 7092
            2.6.33  Finite intersections   cfi 7103
            2.6.34  Supremum and infimum   csup 7117
            2.6.35  Ordinal isomorphism   ordiso2 7170
            2.6.36  Disjoint union   cdju 7172
                  2.6.36.1  Disjoint union   cdju 7172
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 7180
                  2.6.36.3  Universal property of the disjoint union   djuss 7205
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7228
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7237
                  2.6.36.6  Countable sets   0ct 7242
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7254
            2.6.38  Omniscient sets   comni 7269
            2.6.39  Markov's principle   cmarkov 7286
            2.6.40  Weakly omniscient sets   cwomni 7298
            2.6.41  Cardinal numbers   ccrd 7317
            2.6.42  Axiom of Choice equivalents   wac 7355
            2.6.43  Cardinal number arithmetic   endjudisj 7360
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7371
            2.6.45  Excluded middle and the power set of a singleton   iftrueb01 7376
            2.6.46  Apartness relations   wap 7401
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7416
​​*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 7427
            4.1.2  Final derivation of real and complex number postulates   axcnex 8014
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 8058
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 8091
            4.2.2  Infinity and the extended real number system   cpnf 8146
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 8181
            4.2.4  Ordering on reals   lttr 8188
            4.2.5  Initial properties of the complex numbers   mul12 8243
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8272
            4.3.2  Subtraction   cmin 8285
            4.3.3  Multiplication   kcnktkm1cn 8497
            4.3.4  Ordering on reals (cont.)   ltadd2 8534
            4.3.5  Real Apartness   creap 8689
            4.3.6  Complex Apartness   cap 8696
            4.3.7  Reciprocals   recextlem1 8766
            4.3.8  Division   cdiv 8787
            4.3.9  Ordering on reals (cont.)   ltp1 8959
            4.3.10  Suprema   lbreu 9060
            4.3.11  Imaginary and complex number properties   crap0 9073
            4.3.12  Function operation analogue theorems   ofnegsub 9077
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 9078
            4.4.2  Principle of mathematical induction   nnind 9094
            ​*4.4.3  Decimal representation of numbers   c2 9129
            ​*4.4.4  Some properties of specific numbers   neg1cn 9183
            4.4.5  Simple number properties   halfcl 9305
            4.4.6  The Archimedean property   arch 9334
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9337
            ​*4.4.8  Extended nonnegative integers   cxnn0 9400
            4.4.9  Integers (as a subset of complex numbers)   cz 9414
            4.4.10  Decimal arithmetic   cdc 9546
            4.4.11  Upper sets of integers   cuz 9690
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9782
            4.4.13  Complex numbers as pairs of reals   cnref1o 9814
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9817
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9933
            4.5.3  Real number intervals   cioo 10052
            4.5.4  Finite intervals of integers   cfz 10172
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10276
            4.5.6  Half-open integer ranges   cfzo 10306
            4.5.7  Rational numbers (cont.)   qtri3or 10427
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10455
            4.6.2  The modulo (remainder) operation   cmo 10511
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10588
            4.6.4  Strong induction over upper sets of integers   uzsinds 10633
            4.6.5  The infinite sequence builder "seq"   cseq 10636
            4.6.6  Integer powers   cexp 10727
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10908
            4.6.8  Factorial function   cfa 10914
            4.6.9  The binomial coefficient operation   cbc 10936
            4.6.10  The ` # ` (set size) function   chash 10964
                  4.6.10.1  Proper unordered pairs and triples (sets of size 2 and 3)   hash2en 11032
                  4.6.10.2  Functions with a domain containing at least two different elements   fundm2domnop0 11034
      ​​*4.7  Words over a set
            4.7.1  Definitions and basic theorems   cword 11038
            4.7.2  Last symbol of a word   clsw 11082
            4.7.3  Concatenations of words   cconcat 11091
            4.7.4  Singleton words   cs1 11114
            4.7.5  Concatenations with singleton words   ccatws1cl 11131
            4.7.6  Subwords/substrings   csubstr 11143
            4.7.7  Prefixes of a word   cpfx 11170
            4.7.8  Subwords of subwords   swrdswrdlem 11202
            4.7.9  Subwords and concatenations   pfxcctswrd 11208
            4.7.10  Subwords of concatenations   swrdccatfn 11222
            4.7.11  Longer string literals   cs2 11247
      ​4.8  Elementary real and complex functions
            4.8.1  The "shift" operation   cshi 11291
            4.8.2  Real and imaginary parts; conjugate   ccj 11316
            4.8.3  Sequence convergence   caucvgrelemrec 11456
            4.8.4  Square root; absolute value   csqrt 11473
            4.8.5  The maximum of two real numbers   maxcom 11680
            4.8.6  The minimum of two real numbers   mincom 11706
            4.8.7  The maximum of two extended reals   xrmaxleim 11721
            4.8.8  The minimum of two extended reals   xrnegiso 11739
      ​4.9  Elementary limits and convergence
            4.9.1  Limits   cli 11755
            4.9.2  Finite and infinite sums   csu 11830
            4.9.3  The binomial theorem   binomlem 11960
            4.9.4  Infinite sums (cont.)   isumshft 11967
            4.9.5  Miscellaneous converging and diverging sequences   divcnv 11974
            4.9.6  Arithmetic series   arisum 11975
            4.9.7  Geometric series   expcnvap0 11979
            4.9.8  Ratio test for infinite series convergence   cvgratnnlembern 12000
            4.9.9  Mertens' theorem   mertenslemub 12011
            4.9.10  Finite and infinite products   prodf 12015
                  4.9.10.1  Product sequences   prodf 12015
                  4.9.10.2  Non-trivial convergence   ntrivcvgap 12025
                  4.9.10.3  Complex products   cprod 12027
                  4.9.10.4  Finite products   fprodseq 12060
      ​4.10  Elementary trigonometry
            4.10.1  The exponential, sine, and cosine functions   ce 12119
                  4.10.1.1  The circle constant (tau = 2 pi)   ctau 12252
            4.10.2  _e is irrational   eirraplem 12254
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 12264
            ​*5.1.2  Even and odd numbers   evenelz 12344
            5.1.3  The division algorithm   divalglemnn 12395
            5.1.4  Bit sequences   cbits 12417
            5.1.5  The greatest common divisor operator   cgcd 12440
            5.1.6  Bézout's identity   bezoutlemnewy 12483
            5.1.7  Decidable sets of integers   nnmindc 12521
            5.1.8  Algorithms   nn0seqcvgd 12529
            5.1.9  Euclid's Algorithm   eucalgval2 12541
            ​*5.1.10  The least common multiple   clcm 12548
            ​*5.1.11  Coprimality and Euclid's lemma   coprmgcdb 12576
            5.1.12  Cancellability of congruences   congr 12588
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12595
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12632
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12649
            5.2.4  Properties of the canonical representation of a rational   cnumer 12669
            5.2.5  Euler's theorem   codz 12696
            5.2.6  Arithmetic modulo a prime number   modprm1div 12736
            5.2.7  Pythagorean Triples   coprimeprodsq 12746
            5.2.8  The prime count function   cpc 12773
            5.2.9  Pocklington's theorem   prmpwdvds 12844
            5.2.10  Infinite primes theorem   infpnlem1 12848
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 12852
            5.2.12  Lagrange's four-square theorem   cgz 12858
            5.2.13  Decimal arithmetic (cont.)   dec2dvds 12900
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12929
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 12994
            6.1.2  Slot definitions   cplusg 13076
            6.1.3  Definition of the structure product   crest 13238
            6.1.4  Definition of the structure quotient   cimas 13298
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 13352
            ​*7.1.2  Identity elements   mgmidmo 13371
            ​*7.1.3  Iterated sums in a magma   fngsum 13387
            ​*7.1.4  Semigroups   csgrp 13400
            ​*7.1.5  Definition and basic properties of monoids   cmnd 13415
            7.1.6  Monoid homomorphisms and submonoids   cmhm 13456
            ​*7.1.7  Iterated sums in a monoid   gsumvallem2 13492
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 13499
            ​*7.2.2  Group multiple operation   cmg 13622
            7.2.3  Subgroups and Quotient groups   csubg 13670
            7.2.4  Elementary theory of group homomorphisms   cghm 13743
            7.2.5  Abelian groups   ccmn 13787
                  7.2.5.1  Definition and basic properties   ccmn 13787
                  7.2.5.2  Group sum operation   gsumfzreidx 13840
      ​7.3  Rings
            7.3.1  Multiplicative Group   cmgp 13849
            ​*7.3.2  Non-unital rings ("rngs")   crng 13861
            ​*7.3.3  Ring unity (multiplicative identity)   cur 13888
            7.3.4  Semirings   csrg 13892
            7.3.5  Definition and basic properties of unital rings   crg 13925
            7.3.6  Opposite ring   coppr 13996
            7.3.7  Divisibility   cdsr 14015
            7.3.8  Ring homomorphisms   crh 14079
            7.3.9  Nonzero rings and zero rings   cnzr 14108
            7.3.10  Local rings   clring 14119
            7.3.11  Subrings   csubrng 14126
                  7.3.11.1  Subrings of non-unital rings   csubrng 14126
                  7.3.11.2  Subrings of unital rings   csubrg 14146
            7.3.12  Left regular elements and domains   crlreg 14184
      ​7.4  Division rings and fields
            7.4.1  Ring apartness   capr 14209
      ​7.5  Left modules
            7.5.1  Definition and basic properties   clmod 14216
            7.5.2  Subspaces and spans in a left module   clss 14281
      ​7.6  Subring algebras and ideals
            7.6.1  Subring algebras   csra 14362
            7.6.2  Ideals and spans   clidl 14396
            7.6.3  Two-sided ideals and quotient rings   c2idl 14428
            7.6.4  Principal ideal rings. Divisibility in the integers   rspsn 14463
      ​7.7  The complex numbers as an algebraic extensible structure
            7.7.1  Definition and basic properties   cpsmet 14464
            ​*7.7.2  Ring of integers   czring 14519
            7.7.3  Algebraic constructions based on the complex numbers   czrh 14540
​​*PART 8  BASIC LINEAR ALGEBRA
      ​8.1  Abstract multivariate polynomials
            8.1.1  Definition and basic properties   cmps 14590
​PART 9  BASIC TOPOLOGY
      ​9.1  Topology
            ​*9.1.1  Topological spaces   ctop 14636
                  9.1.1.1  Topologies   ctop 14636
                  9.1.1.2  Topologies on sets   ctopon 14649
                  9.1.1.3  Topological spaces   ctps 14669
            9.1.2  Topological bases   ctb 14681
            9.1.3  Examples of topologies   distop 14724
            9.1.4  Closure and interior   ccld 14731
            9.1.5  Neighborhoods   cnei 14777
            9.1.6  Subspace topologies   restrcl 14806
            9.1.7  Limits and continuity in topological spaces   ccn 14824
            9.1.8  Product topologies   ctx 14891
            9.1.9  Continuous function-builders   cnmptid 14920
            9.1.10  Homeomorphisms   chmeo 14939
      ​9.2  Metric spaces
            9.2.1  Pseudometric spaces   psmetrel 14961
            9.2.2  Basic metric space properties   cxms 14975
            9.2.3  Metric space balls   blfvalps 15024
            9.2.4  Open sets of a metric space   mopnrel 15080
            9.2.5  Continuity in metric spaces   metcnp3 15150
            9.2.6  Topology on the reals   qtopbasss 15160
            9.2.7  Topological definitions using the reals   ccncf 15209
​PART 10  BASIC REAL AND COMPLEX ANALYSIS
      ​10.1  Continuity
            10.1.1  Dedekind cuts   dedekindeulemuub 15256
            10.1.2  Intermediate value theorem   ivthinclemlm 15273
      ​10.2  Derivatives
            10.2.1  Real and complex differentiation   climc 15293
                  10.2.1.1  Derivatives of functions of one complex or real variable   climc 15293
​PART 11  BASIC REAL AND COMPLEX FUNCTIONS
      ​11.1  Polynomials
            11.1.1  Elementary properties of complex polynomials   cply 15367
      ​11.2  Basic trigonometry
            11.2.1  The exponential, sine, and cosine functions (cont.)   efcn 15407
            11.2.2  Properties of pi = 3.14159...   pilem1 15418
            11.2.3  The natural logarithm on complex numbers   clog 15495
            ​*11.2.4  Logarithms to an arbitrary base   clogb 15582
            11.2.5  Quartic binomial expansion   binom4 15618
      ​11.3  Basic number theory
            11.3.1  Wilson's theorem   wilthlem1 15619
            11.3.2  Number-theoretical functions   csgm 15620
            11.3.3  Perfect Number Theorem   mersenne 15636
            ​*11.3.4  Quadratic residues and the Legendre symbol   clgs 15641
            ​*11.3.5  Gauss' Lemma   gausslemma2dlem0a 15693
            11.3.6  Quadratic reciprocity   lgseisenlem1 15714
            11.3.7  All primes 4n+1 are the sum of two squares   2sqlem1 15758
​PART 12  GRAPH THEORY
      ​12.1  Vertices and edges
            12.1.1  The edge function extractor for extensible structures   cedgf 15770
            12.1.2  Vertices and indexed edges   cvtx 15778
                  12.1.2.1  Definitions and basic properties   cvtx 15778
                  12.1.2.2  The vertices and edges of a graph represented as ordered pair   opvtxval 15787
                  12.1.2.3  The vertices and edges of a graph represented as extensible structure   funvtxdm2domval 15795
                  12.1.2.4  Degenerated cases of representations of graphs   vtxval0 15819
            12.1.3  Edges as range of the edge function   cedg 15823
      ​12.2  Undirected graphs
            12.2.1  Undirected hypergraphs   cuhgr 15832
            12.2.2  Undirected pseudographs and multigraphs   cupgr 15856
            ​*12.2.3  Loop-free graphs   umgrislfupgrenlem 15893
            12.2.4  Edges as subsets of vertices of graphs   uhgredgiedgb 15897
            ​*12.2.5  Undirected simple graphs   cuspgr 15916
​PART 13  GUIDES AND MISCELLANEA
      ​13.1  Guides (conventions, explanations, and examples)
            ​*13.1.1  Conventions   conventions 15995
            13.1.2  Definitional examples   ex-or 15996
​PART 14  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​14.1  Mathboxes for user contributions
            14.1.1  Mathbox guidelines   mathbox 16006
      ​14.2  Mathbox for BJ
            14.2.1  Propositional calculus   bj-nnsn 16007
                  ​*14.2.1.1  Stable formulas   bj-trst 16013
                  14.2.1.2  Decidable formulas   bj-trdc 16026
            14.2.2  Predicate calculus   bj-ex 16036
            14.2.3  Set theorey miscellaneous   bj-el2oss1o 16048
            ​*14.2.4  Extensionality   bj-vtoclgft 16049
            ​*14.2.5  Decidability of classes   wdcin 16067
            14.2.6  Disjoint union   djucllem 16074
            14.2.7  Miscellaneous   funmptd 16077
            ​*14.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 16085
                  *14.2.8.1  Bounded formulas   wbd 16085
                  ​*14.2.8.2  Bounded classes   wbdc 16113
            ​*14.2.9  CZF: Bounded separation   ax-bdsep 16157
                  14.2.9.1  Delta_0-classical logic   ax-bj-d0cl 16197
                  14.2.9.2  Inductive classes and the class of natural number ordinals   wind 16199
                  ​*14.2.9.3  The first three Peano postulates   bj-peano2 16212
            ​*14.2.10  CZF: Infinity   ax-infvn 16214
                  *14.2.10.1  The set of natural number ordinals   ax-infvn 16214
                  ​*14.2.10.2  Peano's fifth postulate   bdpeano5 16216
                  ​*14.2.10.3  Bounded induction and Peano's fourth postulate   findset 16218
            ​*14.2.11  CZF: Set induction   setindft 16238
                  *14.2.11.1  Set induction   setindft 16238
                  ​*14.2.11.2  Full induction   bj-findis 16252
            ​*14.2.12  CZF: Strong collection   ax-strcoll 16255
            ​*14.2.13  CZF: Subset collection   ax-sscoll 16260
            14.2.14  Real numbers   ax-ddkcomp 16262
      ​14.3  Mathbox for Jim Kingdon
            14.3.1  Propositional and predicate logic   nnnotnotr 16263
            14.3.2  The sizes of sets   1dom1el 16264
            14.3.3  The power set of a singleton   pwtrufal 16274
            14.3.4  Omniscience of NN+oo   0nninf 16281
            14.3.5  Schroeder-Bernstein Theorem   exmidsbthrlem 16301
            14.3.6  Real and complex numbers   qdencn 16306
            ​*14.3.7  Analytic omniscience principles   trilpolemclim 16315
            14.3.8  Supremum and infimum   supfz 16350
            14.3.9  Circle constant   taupi 16352
      ​14.4  Mathbox for Mykola Mostovenko
      ​14.5  Mathbox for David A. Wheeler
            14.5.1  Testable propositions   dftest 16354
            ​*14.5.2  Allsome quantifier   walsi 16355