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 615
            1.2.6  Logical disjunction   wo 710
            1.2.7  Stable propositions   wstab 832
            1.2.8  Decidable propositions   wdc 836
            ​*1.2.9  Theorems of decidable propositions   const 854
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 918
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 980
            1.2.12  True and false constants   wal 1371
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1371
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1372
                  1.2.12.3  Define the true and false constants   wtru 1374
            1.2.13  Logical 'xor'   wxo 1395
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1421
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1443
            1.2.16  Logical implication (continued)   syl6an 1454
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1471
            ​*1.3.2  Equality predicate (continued)   weq 1527
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1550
            1.3.4  Introduce Axiom of Existence   ax-i9 1554
            1.3.5  Additional intuitionistic axioms   ax-ial 1558
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1560
            1.3.7  The existential quantifier   19.8a 1614
            1.3.8  Equality theorems without distinct variables   a9e 1720
            1.3.9  Axioms ax-10 and ax-11   ax10o 1739
            1.3.10  Substitution (without distinct variables)   wsb 1786
            1.3.11  Theorems using axiom ax-11   equs5a 1818
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1835
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1846
            1.4.3  More theorems related to ax-11 and substitution   albidv 1848
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1882
            1.4.5  More substitution theorems   hbs1 1967
            1.4.6  Existential uniqueness   weu 2055
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2153
      ​​*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 2188
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2192
                  2.1.2.1  Elementary properties of class abstractions   eqabdv 2335
            2.1.3  Class form not-free predicate   wnfc 2336
            2.1.4  Negated equality and membership   wne 2377
                  2.1.4.1  Negated equality   wne 2377
                  2.1.4.2  Negated membership   wnel 2472
            2.1.5  Restricted quantification   wral 2485
            2.1.6  The universal class   cvv 2773
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2985
            2.1.8  Russell's Paradox   ru 3001
            2.1.9  Proper substitution of classes for sets   wsbc 3002
            2.1.10  Proper substitution of classes for sets into classes   csb 3097
            2.1.11  Define basic set operations and relations   cdif 3167
            2.1.12  Subclasses and subsets   df-ss 3183
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3287
                  2.1.13.1  The difference of two classes   dfdif3 3287
                  2.1.13.2  The union of two classes   elun 3318
                  2.1.13.3  The intersection of two classes   elin 3360
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3408
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3443
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3457
            2.1.14  The empty set   c0 3464
            2.1.15  Conditional operator   cif 3575
            2.1.16  Power classes   cpw 3620
            2.1.17  Unordered and ordered pairs   csn 3637
            2.1.18  The union of a class   cuni 3855
            2.1.19  The intersection of a class   cint 3890
            2.1.20  Indexed union and intersection   ciun 3932
            2.1.21  Disjointness   wdisj 4026
            2.1.22  Binary relations   wbr 4050
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4111
            2.1.24  Transitive classes   wtr 4149
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4166
            2.2.2  Introduce the Axiom of Separation   ax-sep 4169
            2.2.3  Derive the Null Set Axiom   zfnuleu 4175
            2.2.4  Theorems requiring subset and intersection existence   nalset 4181
            2.2.5  Theorems requiring empty set existence   class2seteq 4214
            2.2.6  Collection principle   bnd 4223
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4225
            2.3.2  A notation for excluded middle   wem 4245
            2.3.3  Axiom of Pairing   ax-pr 4260
            2.3.4  Ordered pair theorem   opm 4285
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4309
            2.3.6  Power class of union and intersection   pwin 4336
            2.3.7  Epsilon and identity relations   cep 4341
            ​*2.3.8  Partial and total orderings   wpo 4348
            2.3.9  Founded and set-like relations   wfrfor 4381
            2.3.10  Ordinals   word 4416
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4487
            2.4.2  Ordinals (continued)   ordon 4541
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4587
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4592
            2.5.3  Transfinite induction   tfi 4637
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4643
            2.6.2  The natural numbers   com 4645
            2.6.3  Peano's postulates   peano1 4649
            2.6.4  Finite induction (for finite ordinals)   find 4654
            2.6.5  The Natural Numbers (continued)   nn0suc 4659
            2.6.6  Relations   cxp 4680
            2.6.7  Definite description binder (inverted iota)   cio 5238
            2.6.8  Functions   wfun 5273
            2.6.9  Cantor's Theorem   canth 5909
            2.6.10  Restricted iota (description binder)   crio 5910
            2.6.11  Operations   co 5956
            2.6.12  Maps-to notation   elmpocl 6153
            2.6.13  Function operation   cof 6168
            2.6.14  Functions (continued)   resfunexgALT 6205
            2.6.15  First and second members of an ordered pair   c1st 6236
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6336
            2.6.17  Function transposition   ctpos 6342
            2.6.18  Undefined values   pwuninel2 6380
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6382
            2.6.20  "Strong" transfinite recursion   crecs 6402
            2.6.21  Recursive definition generator   crdg 6467
            2.6.22  Finite recursion   cfrec 6488
            2.6.23  Ordinal arithmetic   c1o 6507
            2.6.24  Natural number arithmetic   nna0 6572
            2.6.25  Equivalence relations and classes   wer 6629
            2.6.26  The mapping operation   cmap 6747
            2.6.27  Infinite Cartesian products   cixp 6797
            2.6.28  Equinumerosity   cen 6837
            2.6.29  Equinumerosity (cont.)   xpf1o 6955
            2.6.30  Pigeonhole Principle   phplem1 6963
            2.6.31  Finite sets   fict 6979
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 7073
            2.6.33  Finite intersections   cfi 7084
            2.6.34  Supremum and infimum   csup 7098
            2.6.35  Ordinal isomorphism   ordiso2 7151
            2.6.36  Disjoint union   cdju 7153
                  2.6.36.1  Disjoint union   cdju 7153
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 7161
                  2.6.36.3  Universal property of the disjoint union   djuss 7186
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7209
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7218
                  2.6.36.6  Countable sets   0ct 7223
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7235
            2.6.38  Omniscient sets   comni 7250
            2.6.39  Markov's principle   cmarkov 7267
            2.6.40  Weakly omniscient sets   cwomni 7279
            2.6.41  Cardinal numbers   ccrd 7298
            2.6.42  Axiom of Choice equivalents   wac 7332
            2.6.43  Cardinal number arithmetic   endjudisj 7337
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7348
            2.6.45  Excluded middle and the power set of a singleton   pw1on 7353
            2.6.46  Apartness relations   wap 7374
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7389
​​*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 7400
            4.1.2  Final derivation of real and complex number postulates   axcnex 7987
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 8031
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 8064
            4.2.2  Infinity and the extended real number system   cpnf 8119
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 8154
            4.2.4  Ordering on reals   lttr 8161
            4.2.5  Initial properties of the complex numbers   mul12 8216
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8245
            4.3.2  Subtraction   cmin 8258
            4.3.3  Multiplication   kcnktkm1cn 8470
            4.3.4  Ordering on reals (cont.)   ltadd2 8507
            4.3.5  Real Apartness   creap 8662
            4.3.6  Complex Apartness   cap 8669
            4.3.7  Reciprocals   recextlem1 8739
            4.3.8  Division   cdiv 8760
            4.3.9  Ordering on reals (cont.)   ltp1 8932
            4.3.10  Suprema   lbreu 9033
            4.3.11  Imaginary and complex number properties   crap0 9046
            4.3.12  Function operation analogue theorems   ofnegsub 9050
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 9051
            4.4.2  Principle of mathematical induction   nnind 9067
            ​*4.4.3  Decimal representation of numbers   c2 9102
            ​*4.4.4  Some properties of specific numbers   neg1cn 9156
            4.4.5  Simple number properties   halfcl 9278
            4.4.6  The Archimedean property   arch 9307
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9310
            ​*4.4.8  Extended nonnegative integers   cxnn0 9373
            4.4.9  Integers (as a subset of complex numbers)   cz 9387
            4.4.10  Decimal arithmetic   cdc 9519
            4.4.11  Upper sets of integers   cuz 9663
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9755
            4.4.13  Complex numbers as pairs of reals   cnref1o 9787
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9790
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9906
            4.5.3  Real number intervals   cioo 10025
            4.5.4  Finite intervals of integers   cfz 10145
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10249
            4.5.6  Half-open integer ranges   cfzo 10279
            4.5.7  Rational numbers (cont.)   qtri3or 10400
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10428
            4.6.2  The modulo (remainder) operation   cmo 10484
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10561
            4.6.4  Strong induction over upper sets of integers   uzsinds 10606
            4.6.5  The infinite sequence builder "seq"   cseq 10609
            4.6.6  Integer powers   cexp 10700
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10881
            4.6.8  Factorial function   cfa 10887
            4.6.9  The binomial coefficient operation   cbc 10909
            4.6.10  The ` # ` (set size) function   chash 10937
                  4.6.10.1  Proper unordered pairs and triples (sets of size 2 and 3)   hash2en 11005
                  4.6.10.2  Functions with a domain containing at least two different elements   fundm2domnop0 11007
      ​​*4.7  Words over a set
            4.7.1  Definitions and basic theorems   cword 11011
            4.7.2  Last symbol of a word   clsw 11055
            4.7.3  Concatenations of words   cconcat 11064
            4.7.4  Singleton words   cs1 11087
            4.7.5  Concatenations with singleton words   ccatws1cl 11104
            4.7.6  Subwords/substrings   csubstr 11116
            4.7.7  Prefixes of a word   cpfx 11143
            4.7.8  Subwords of subwords   swrdswrdlem 11175
            4.7.9  Subwords and concatenations   pfxcctswrd 11181
      ​4.8  Elementary real and complex functions
            4.8.1  The "shift" operation   cshi 11195
            4.8.2  Real and imaginary parts; conjugate   ccj 11220
            4.8.3  Sequence convergence   caucvgrelemrec 11360
            4.8.4  Square root; absolute value   csqrt 11377
            4.8.5  The maximum of two real numbers   maxcom 11584
            4.8.6  The minimum of two real numbers   mincom 11610
            4.8.7  The maximum of two extended reals   xrmaxleim 11625
            4.8.8  The minimum of two extended reals   xrnegiso 11643
      ​4.9  Elementary limits and convergence
            4.9.1  Limits   cli 11659
            4.9.2  Finite and infinite sums   csu 11734
            4.9.3  The binomial theorem   binomlem 11864
            4.9.4  Infinite sums (cont.)   isumshft 11871
            4.9.5  Miscellaneous converging and diverging sequences   divcnv 11878
            4.9.6  Arithmetic series   arisum 11879
            4.9.7  Geometric series   expcnvap0 11883
            4.9.8  Ratio test for infinite series convergence   cvgratnnlembern 11904
            4.9.9  Mertens' theorem   mertenslemub 11915
            4.9.10  Finite and infinite products   prodf 11919
                  4.9.10.1  Product sequences   prodf 11919
                  4.9.10.2  Non-trivial convergence   ntrivcvgap 11929
                  4.9.10.3  Complex products   cprod 11931
                  4.9.10.4  Finite products   fprodseq 11964
      ​4.10  Elementary trigonometry
            4.10.1  The exponential, sine, and cosine functions   ce 12023
                  4.10.1.1  The circle constant (tau = 2 pi)   ctau 12156
            4.10.2  _e is irrational   eirraplem 12158
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 12168
            ​*5.1.2  Even and odd numbers   evenelz 12248
            5.1.3  The division algorithm   divalglemnn 12299
            5.1.4  Bit sequences   cbits 12321
            5.1.5  The greatest common divisor operator   cgcd 12344
            5.1.6  Bézout's identity   bezoutlemnewy 12387
            5.1.7  Decidable sets of integers   nnmindc 12425
            5.1.8  Algorithms   nn0seqcvgd 12433
            5.1.9  Euclid's Algorithm   eucalgval2 12445
            ​*5.1.10  The least common multiple   clcm 12452
            ​*5.1.11  Coprimality and Euclid's lemma   coprmgcdb 12480
            5.1.12  Cancellability of congruences   congr 12492
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12499
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12536
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12553
            5.2.4  Properties of the canonical representation of a rational   cnumer 12573
            5.2.5  Euler's theorem   codz 12600
            5.2.6  Arithmetic modulo a prime number   modprm1div 12640
            5.2.7  Pythagorean Triples   coprimeprodsq 12650
            5.2.8  The prime count function   cpc 12677
            5.2.9  Pocklington's theorem   prmpwdvds 12748
            5.2.10  Infinite primes theorem   infpnlem1 12752
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 12756
            5.2.12  Lagrange's four-square theorem   cgz 12762
            5.2.13  Decimal arithmetic (cont.)   dec2dvds 12804
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12833
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 12898
            6.1.2  Slot definitions   cplusg 12979
            6.1.3  Definition of the structure product   crest 13141
            6.1.4  Definition of the structure quotient   cimas 13201
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 13255
            ​*7.1.2  Identity elements   mgmidmo 13274
            ​*7.1.3  Iterated sums in a magma   fngsum 13290
            ​*7.1.4  Semigroups   csgrp 13303
            ​*7.1.5  Definition and basic properties of monoids   cmnd 13318
            7.1.6  Monoid homomorphisms and submonoids   cmhm 13359
            ​*7.1.7  Iterated sums in a monoid   gsumvallem2 13395
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 13402
            ​*7.2.2  Group multiple operation   cmg 13525
            7.2.3  Subgroups and Quotient groups   csubg 13573
            7.2.4  Elementary theory of group homomorphisms   cghm 13646
            7.2.5  Abelian groups   ccmn 13690
                  7.2.5.1  Definition and basic properties   ccmn 13690
                  7.2.5.2  Group sum operation   gsumfzreidx 13743
      ​7.3  Rings
            7.3.1  Multiplicative Group   cmgp 13752
            ​*7.3.2  Non-unital rings ("rngs")   crng 13764
            ​*7.3.3  Ring unity (multiplicative identity)   cur 13791
            7.3.4  Semirings   csrg 13795
            7.3.5  Definition and basic properties of unital rings   crg 13828
            7.3.6  Opposite ring   coppr 13899
            7.3.7  Divisibility   cdsr 13918
            7.3.8  Ring homomorphisms   crh 13982
            7.3.9  Nonzero rings and zero rings   cnzr 14011
            7.3.10  Local rings   clring 14022
            7.3.11  Subrings   csubrng 14029
                  7.3.11.1  Subrings of non-unital rings   csubrng 14029
                  7.3.11.2  Subrings of unital rings   csubrg 14049
            7.3.12  Left regular elements and domains   crlreg 14087
      ​7.4  Division rings and fields
            7.4.1  Ring apartness   capr 14112
      ​7.5  Left modules
            7.5.1  Definition and basic properties   clmod 14119
            7.5.2  Subspaces and spans in a left module   clss 14184
      ​7.6  Subring algebras and ideals
            7.6.1  Subring algebras   csra 14265
            7.6.2  Ideals and spans   clidl 14299
            7.6.3  Two-sided ideals and quotient rings   c2idl 14331
            7.6.4  Principal ideal rings. Divisibility in the integers   rspsn 14366
      ​7.7  The complex numbers as an algebraic extensible structure
            7.7.1  Definition and basic properties   cpsmet 14367
            ​*7.7.2  Ring of integers   czring 14422
            7.7.3  Algebraic constructions based on the complex numbers   czrh 14443
​​*PART 8  BASIC LINEAR ALGEBRA
      ​8.1  Abstract multivariate polynomials
            8.1.1  Definition and basic properties   cmps 14493
​PART 9  BASIC TOPOLOGY
      ​9.1  Topology
            ​*9.1.1  Topological spaces   ctop 14539
                  9.1.1.1  Topologies   ctop 14539
                  9.1.1.2  Topologies on sets   ctopon 14552
                  9.1.1.3  Topological spaces   ctps 14572
            9.1.2  Topological bases   ctb 14584
            9.1.3  Examples of topologies   distop 14627
            9.1.4  Closure and interior   ccld 14634
            9.1.5  Neighborhoods   cnei 14680
            9.1.6  Subspace topologies   restrcl 14709
            9.1.7  Limits and continuity in topological spaces   ccn 14727
            9.1.8  Product topologies   ctx 14794
            9.1.9  Continuous function-builders   cnmptid 14823
            9.1.10  Homeomorphisms   chmeo 14842
      ​9.2  Metric spaces
            9.2.1  Pseudometric spaces   psmetrel 14864
            9.2.2  Basic metric space properties   cxms 14878
            9.2.3  Metric space balls   blfvalps 14927
            9.2.4  Open sets of a metric space   mopnrel 14983
            9.2.5  Continuity in metric spaces   metcnp3 15053
            9.2.6  Topology on the reals   qtopbasss 15063
            9.2.7  Topological definitions using the reals   ccncf 15112
​PART 10  BASIC REAL AND COMPLEX ANALYSIS
      ​10.1  Continuity
            10.1.1  Dedekind cuts   dedekindeulemuub 15159
            10.1.2  Intermediate value theorem   ivthinclemlm 15176
      ​10.2  Derivatives
            10.2.1  Real and complex differentiation   climc 15196
                  10.2.1.1  Derivatives of functions of one complex or real variable   climc 15196
​PART 11  BASIC REAL AND COMPLEX FUNCTIONS
      ​11.1  Polynomials
            11.1.1  Elementary properties of complex polynomials   cply 15270
      ​11.2  Basic trigonometry
            11.2.1  The exponential, sine, and cosine functions (cont.)   efcn 15310
            11.2.2  Properties of pi = 3.14159...   pilem1 15321
            11.2.3  The natural logarithm on complex numbers   clog 15398
            ​*11.2.4  Logarithms to an arbitrary base   clogb 15485
            11.2.5  Quartic binomial expansion   binom4 15521
      ​11.3  Basic number theory
            11.3.1  Wilson's theorem   wilthlem1 15522
            11.3.2  Number-theoretical functions   csgm 15523
            11.3.3  Perfect Number Theorem   mersenne 15539
            ​*11.3.4  Quadratic residues and the Legendre symbol   clgs 15544
            ​*11.3.5  Gauss' Lemma   gausslemma2dlem0a 15596
            11.3.6  Quadratic reciprocity   lgseisenlem1 15617
            11.3.7  All primes 4n+1 are the sum of two squares   2sqlem1 15661
​PART 12  GRAPH THEORY
      ​12.1  Vertices and edges
            12.1.1  The edge function extractor for extensible structures   cedgf 15673
            12.1.2  Vertices and indexed edges   cvtx 15681
                  12.1.2.1  Definitions and basic properties   cvtx 15681
                  12.1.2.2  The vertices and edges of a graph represented as ordered pair   opvtxval 15690
                  12.1.2.3  The vertices and edges of a graph represented as extensible structure   funvtxdm2domval 15698
                  12.1.2.4  Degenerated cases of representations of graphs   vtxval0 15720
            12.1.3  Edges as range of the edge function   cedg 15724
      ​12.2  Undirected graphs
            12.2.1  Undirected hypergraphs   cuhgr 15733
            12.2.2  Undirected pseudographs and multigraphs   cupgr 15757
​PART 13  GUIDES AND MISCELLANEA
      ​13.1  Guides (conventions, explanations, and examples)
            ​*13.1.1  Conventions   conventions 15791
            13.1.2  Definitional examples   ex-or 15792
​PART 14  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​14.1  Mathboxes for user contributions
            14.1.1  Mathbox guidelines   mathbox 15802
      ​14.2  Mathbox for BJ
            14.2.1  Propositional calculus   bj-nnsn 15803
                  ​*14.2.1.1  Stable formulas   bj-trst 15809
                  14.2.1.2  Decidable formulas   bj-trdc 15822
            14.2.2  Predicate calculus   bj-ex 15832
            14.2.3  Set theorey miscellaneous   bj-el2oss1o 15844
            ​*14.2.4  Extensionality   bj-vtoclgft 15845
            ​*14.2.5  Decidability of classes   wdcin 15863
            14.2.6  Disjoint union   djucllem 15870
            14.2.7  Miscellaneous   funmptd 15873
            ​*14.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 15882
                  *14.2.8.1  Bounded formulas   wbd 15882
                  ​*14.2.8.2  Bounded classes   wbdc 15910
            ​*14.2.9  CZF: Bounded separation   ax-bdsep 15954
                  14.2.9.1  Delta_0-classical logic   ax-bj-d0cl 15994
                  14.2.9.2  Inductive classes and the class of natural number ordinals   wind 15996
                  ​*14.2.9.3  The first three Peano postulates   bj-peano2 16009
            ​*14.2.10  CZF: Infinity   ax-infvn 16011
                  *14.2.10.1  The set of natural number ordinals   ax-infvn 16011
                  ​*14.2.10.2  Peano's fifth postulate   bdpeano5 16013
                  ​*14.2.10.3  Bounded induction and Peano's fourth postulate   findset 16015
            ​*14.2.11  CZF: Set induction   setindft 16035
                  *14.2.11.1  Set induction   setindft 16035
                  ​*14.2.11.2  Full induction   bj-findis 16049
            ​*14.2.12  CZF: Strong collection   ax-strcoll 16052
            ​*14.2.13  CZF: Subset collection   ax-sscoll 16057
            14.2.14  Real numbers   ax-ddkcomp 16059
      ​14.3  Mathbox for Jim Kingdon
            14.3.1  Propositional and predicate logic   nnnotnotr 16060
            14.3.2  The sizes of sets   1dom1el 16061
            14.3.3  The power set of a singleton   pwtrufal 16069
            14.3.4  Omniscience of NN+oo   0nninf 16076
            14.3.5  Schroeder-Bernstein Theorem   exmidsbthrlem 16096
            14.3.6  Real and complex numbers   qdencn 16101
            ​*14.3.7  Analytic omniscience principles   trilpolemclim 16110
            14.3.8  Supremum and infimum   supfz 16145
            14.3.9  Circle constant   taupi 16147
      ​14.4  Mathbox for Mykola Mostovenko
      ​14.5  Mathbox for David A. Wheeler
            14.5.1  Testable propositions   dftest 16149
            ​*14.5.2  Allsome quantifier   walsi 16150