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