Metamath Proof Explorer

Table of Contents - Database

  1. CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
    1. Pre-logic
    2. Propositional calculus
    3. Other axiomatizations related to classical propositional calculus
    4. Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
    5. Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
    6. Uniqueness and unique existence
    7. Other axiomatizations related to classical predicate calculus
  2. ZF (ZERMELO-FRAENKEL) SET THEORY
    1. ZF Set Theory - start with the Axiom of Extensionality
    2. ZF Set Theory - add the Axiom of Replacement
    3. ZF Set Theory - add the Axiom of Power Sets
    4. ZF Set Theory - add the Axiom of Union
    5. ZF Set Theory - add the Axiom of Regularity
    6. ZF Set Theory - add the Axiom of Infinity
  3. ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY
    1. ZFC Set Theory - add Countable Choice and Dependent Choice
    2. ZFC Set Theory - add the Axiom of Choice
    3. ZFC Axioms with no distinct variable requirements
    4. The Generalized Continuum Hypothesis
  4. TG (TARSKI-GROTHENDIECK) SET THEORY
    1. Inaccessibles
    2. ZFC Set Theory plus the Tarski-Grothendieck Axiom
  5. REAL AND COMPLEX NUMBERS
    1. Construction and axiomatization of real and complex numbers
    2. Derive the basic properties from the field axioms
    3. Real and complex numbers - basic operations
    4. Integer sets
    5. Order sets
    6. Elementary integer functions
    7. Words over a set
    8. Reflexive and transitive closures of relations
    9. Elementary real and complex functions
    10. Elementary limits and convergence
    11. Elementary trigonometry
    12. Cardinality of real and complex number subsets
  6. ELEMENTARY NUMBER THEORY
    1. Elementary properties of divisibility
    2. Elementary prime number theory
  7. BASIC STRUCTURES
    1. Extensible structures
    2. Moore spaces
  8. BASIC CATEGORY THEORY
    1. Categories
    2. Arrows (disjointified hom-sets)
    3. Examples of categories
    4. Categorical constructions
  9. BASIC ORDER THEORY
    1. Dual of an order structure
    2. Preordered sets and directed sets
    3. Partially ordered sets (posets)
    4. Totally ordered sets (tosets)
    5. Lattices
    6. Posets, directed sets, and lattices as relations
  10. BASIC ALGEBRAIC STRUCTURES
    1. Monoids
    2. Groups
    3. Rings
    4. Division rings and fields
    5. Left modules
    6. Vector spaces
    7. Ideals
    8. The complex numbers as an algebraic extensible structure
    9. Generalized pre-Hilbert and Hilbert spaces
  11. BASIC LINEAR ALGEBRA
    1. Vectors and free modules
    2. Associative algebras
    3. Abstract multivariate polynomials
    4. Matrices
    5. The determinant
    6. Polynomial matrices
    7. The characteristic polynomial
  12. BASIC TOPOLOGY
    1. Topology
    2. Filters and filter bases
    3. Uniform Structures and Spaces
    4. Metric spaces
    5. Metric subcomplex vector spaces
  13. BASIC REAL AND COMPLEX ANALYSIS
    1. Continuity
    2. Integrals
    3. Derivatives
  14. BASIC REAL AND COMPLEX FUNCTIONS
    1. Polynomials
    2. Sequences and series
    3. Basic trigonometry
    4. Basic number theory
  15. SURREAL NUMBERS
    1. Sign sequence representation and Alling's axioms
    2. Initial consequences of Alling's axioms
    3. Conway cut representation
    4. Induction and recursion
    5. Surreal arithmetic
  16. ELEMENTARY GEOMETRY
    1. Definition and Tarski's Axioms of Geometry
    2. Tarskian Geometry
    3. Properties of geometries
    4. Geometry in Hilbert spaces
  17. GRAPH THEORY
    1. Vertices and edges
    2. Undirected graphs
    3. Walks, paths and cycles
    4. Eulerian paths and the Konigsberg Bridge problem
    5. The Friendship Theorem
  18. GUIDES AND MISCELLANEA
    1. Guides (conventions, explanations, and examples)
    2. Humor
    3. (Future - to be reviewed and classified)
  19. COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)
    1. Additional material on group theory (deprecated)
    2. Complex vector spaces
    3. Normed complex vector spaces
    4. Operators on complex vector spaces
    5. Inner product (pre-Hilbert) spaces
    6. Complex Banach spaces
    7. Complex Hilbert spaces
    8. Appendix: Typesetting definitions for the tokens in this file
  20. COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
    1. Axiomatization of complex pre-Hilbert spaces
    2. Inner product and norms
    3. Cauchy sequences and completeness axiom
    4. Subspaces and projections
    5. Properties of Hilbert subspaces
    6. Operators on Hilbert spaces
    7. States on a Hilbert lattice and Godowski's equation
    8. Cover relation, atoms, exchange axiom, and modular symmetry
  21. SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
    1. Mathboxes for user contributions
    2. Mathbox for Stefan Allan
    3. Mathbox for Thierry Arnoux
    4. Mathbox for Jonathan Ben-Naim
    5. Mathbox for BTernaryTau
    6. Mathbox for Mario Carneiro
    7. Mathbox for Filip Cernatescu
    8. Mathbox for Paul Chapman
    9. Mathbox for Drahflow
    10. Mathbox for Adrian Ducourtial
    11. Mathbox for Scott Fenton
    12. Mathbox for Gino Giotto
    13. Mathbox for Jeff Hankins
    14. Mathbox for Anthony Hart
    15. Mathbox for Chen-Pang He
    16. Mathbox for Jeff Hoffman
    17. Mathbox for Asger C. Ipsen
    18. Mathbox for BJ
    19. Mathbox for Jim Kingdon
    20. Mathbox for ML
    21. Mathbox for Wolf Lammen
    22. Mathbox for Brendan Leahy
    23. Mathbox for Jeff Madsen
    24. Mathbox for Giovanni Mascellani
    25. Mathbox for Peter Mazsa
    26. Mathbox for Rodolfo Medina
    27. Mathbox for Norm Megill
    28. Mathbox for metakunt
    29. Mathbox for Steven Nguyen
    30. Mathbox for Igor Ieskov
    31. Mathbox for Larry Lesyna
    32. Mathbox for OpenAI
    33. Mathbox for Stefan O'Rear
    34. Mathbox for Noam Pasman
    35. Mathbox for Jon Pennant
    36. Mathbox for Richard Penner
    37. Mathbox for Stanislas Polu
    38. Mathbox for Rohan Ridenour
    39. Mathbox for Steve Rodriguez
    40. Mathbox for Andrew Salmon
    41. Mathbox for Alan Sare
    42. Mathbox for Glauco Siliprandi
    43. Mathbox for Saveliy Skresanov
    44. Mathbox for Ender Ting
    45. Mathbox for Jarvin Udandy
    46. Mathbox for Adhemar
    47. Mathbox for Alexander van der Vekens
    48. Mathbox for Zhi Wang
    49. Mathbox for Emmett Weisz
    50. Mathbox for David A. Wheeler
    51. Mathbox for Kunhao Zheng