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. ELEMENTARY GEOMETRY
    1. Definition and Tarski's Axioms of Geometry
    2. Tarskian Geometry
    3. Properties of geometries
    4. Geometry in Hilbert spaces
  16. 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
  17. GUIDES AND MISCELLANEA
    1. Guides (conventions, explanations, and examples)
    2. Humor
    3. (Future - to be reviewed and classified)
  18. 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
  19. 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
  20. 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 Scott Fenton
    11. Mathbox for Jeff Hankins
    12. Mathbox for Anthony Hart
    13. Mathbox for Chen-Pang He
    14. Mathbox for Jeff Hoffman
    15. Mathbox for Asger C. Ipsen
    16. Mathbox for BJ
    17. Mathbox for Jim Kingdon
    18. Mathbox for ML
    19. Mathbox for Wolf Lammen
    20. Mathbox for Brendan Leahy
    21. Mathbox for Jeff Madsen
    22. Mathbox for Giovanni Mascellani
    23. Mathbox for Peter Mazsa
    24. Mathbox for Rodolfo Medina
    25. Mathbox for Norm Megill
    26. Mathbox for metakunt
    27. Mathbox for Steven Nguyen
    28. Mathbox for Igor Ieskov
    29. Mathbox for Larry Lesyna
    30. Mathbox for OpenAI
    31. Mathbox for Stefan O'Rear
    32. Mathbox for Jon Pennant
    33. Mathbox for Richard Penner
    34. Mathbox for Stanislas Polu
    35. Mathbox for Rohan Ridenour
    36. Mathbox for Steve Rodriguez
    37. Mathbox for Andrew Salmon
    38. Mathbox for Alan Sare
    39. Mathbox for Glauco Siliprandi
    40. Mathbox for Saveliy Skresanov
    41. Mathbox for Jarvin Udandy
    42. Mathbox for Adhemar
    43. Mathbox for Alexander van der Vekens
    44. Mathbox for Zhi Wang
    45. Mathbox for Emmett Weisz
    46. Mathbox for David A. Wheeler
    47. Mathbox for Kunhao Zheng