Metamath Proof Explorer

Table of Contents - 20. SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)

  1. Mathboxes for user contributions
    1. Mathbox guidelines
  2. Mathbox for Stefan Allan
    1. sa-abvi
    2. xfree
    3. xfree2
    4. addltmulALT
  3. Mathbox for Thierry Arnoux
    1. Propositional Calculus - misc additions
    2. Predicate Calculus
    3. General Set Theory
    4. Relations and Functions
    5. Real and Complex Numbers
    6. Decimal expansion
    7. Words over a set - misc additions
    8. Extensible Structures
    9. Algebra
    10. Field Extensions
    11. Matrices
    12. Topology
    13. Uniform Stuctures and Spaces
    14. Topology and algebraic structures
    15. Real and complex functions
    16. Mixed Function/Constant operation
    17. Abstract measure
    18. Integration
    19. Euler's partition theorem
    20. Sequences defined by strong recursion
    21. Fibonacci Numbers
    22. Probability
    23. Signum (sgn or sign) function - misc. additions
    24. Polynomials with real coefficients - misc additions
    25. Descartes's rule of signs
    26. Number Theory
    27. Elementary Geometry
    28. LeftPad Project
  4. Mathbox for Jonathan Ben-Naim
    1. w-bnj17
    2. df-bnj17
    3. c-bnj14
    4. df-bnj14
    5. w-bnj13
    6. df-bnj13
    7. w-bnj15
    8. df-bnj15
    9. c-bnj18
    10. df-bnj18
    11. w-bnj19
    12. df-bnj19
    13. First-order logic and set theory
    14. Well founded induction and recursion
    15. The existence of a minimal element in certain classes
    16. Well-founded induction
    17. Well-founded recursion, part 1 of 3
    18. Well-founded recursion, part 2 of 3
    19. Well-founded recursion, part 3 of 3
  5. Mathbox for BTernaryTau
    1. ZF set theory
    2. Real and complex numbers
    3. Graph theory
  6. Mathbox for Mario Carneiro
    1. Predicate calculus with all distinct variables
    2. Miscellaneous stuff
    3. Derangements and the Subfactorial
    4. The Erdős-Szekeres theorem
    5. Euler's partition theorem
    6. The Kuratowski closure-complement theorem
    7. Retracts and sections
    8. Path-connected and simply connected spaces
    9. Covering maps
    10. Normal numbers
    11. Compactification
    12. Godel-sets of formulas - part 1
    13. Godel-sets of formulas - part 2
    14. Models of ZF
    15. Metamath formal systems
    16. Grammatical formal systems
    17. Models of formal systems
    18. Splitting fields
    19. p-adic number fields
  7. Mathbox for Filip Cernatescu
    1. problem1
    2. problem2
    3. problem3
    4. problem4
    5. problem5
    6. quad3
  8. Mathbox for Paul Chapman
    1. Propositional calculus
    2. Prime numbers
    3. Finite set induction
    4. The ` # ` (set size) function
    5. Real and complex numbers (cont.)
    6. Miscellaneous theorems
  9. Mathbox for Drahflow
  10. Mathbox for Scott Fenton
    1. ZFC Axioms in primitive form
    2. Untangled classes
    3. Extra propositional calculus theorems
    4. Misc. Useful Theorems
    5. Properties of real and complex numbers
    6. Infinite products
    7. Factorial limits
    8. Greatest common divisor and divisibility
    9. Properties of relationships
    10. Properties of functions and mappings
    11. Set induction (or epsilon induction)
    12. Ordinal numbers
    13. Defined equality axioms
    14. Hypothesis builders
    15. (Trans)finite Recursion Theorems
    16. Well-Founded Induction
    17. Ordering Cross Products, Part 2
    18. Ordering Ordinal Sequences
    19. Well-founded zero, successor, and limits
    20. Natural operations on ordinals
    21. Surreal Numbers
    22. Surreal Numbers: Ordering
    23. Surreal Numbers: Birthday Function
    24. Surreal Numbers: Density
    25. Surreal Numbers: Full-Eta Property
    26. Surreal numbers - ordering theorems
    27. Surreal numbers - birthday theorems
    28. Surreal numbers: Conway cuts
    29. Surreal numbers - zero and one
    30. Surreal numbers - cuts and options
    31. Surreal numbers: Cofinality and coinitiality
    32. Surreal numbers: Induction and recursion on one variable
    33. Surreal numbers: Induction and recursion on two variables
    34. Surreal numbers - addition, negation, and subtraction
    35. Quantifier-free definitions
    36. Alternate ordered pairs
    37. Geometry in the Euclidean space
    38. Forward difference
    39. Rank theorems
    40. Hereditarily Finite Sets
  11. Mathbox for Jeff Hankins
    1. Miscellany
    2. Basic topological facts
    3. Topology of the real numbers
    4. Refinements
    5. Neighborhood bases determine topologies
    6. Lattice structure of topologies
    7. Filter bases
    8. Directed sets, nets
  12. Mathbox for Anthony Hart
    1. Propositional Calculus
    2. Predicate Calculus
    3. Miscellaneous single axioms
    4. Connective Symmetry
  13. Mathbox for Chen-Pang He
    1. Ordinal topology
  14. Mathbox for Jeff Hoffman
    1. Inferences for finite induction on generic function values
    2. gdc.mm
  15. Mathbox for Asger C. Ipsen
    1. Continuous nowhere differentiable functions
  16. Mathbox for BJ
    1. Propositional calculus
    2. Modal logic
    3. Provability logic
    4. First-order logic
    5. Set theory
    6. Extended real and complex numbers, real and complex projective lines
    7. Monoids
    8. Affine, Euclidean, and Cartesian geometry
    9. Monoid of endomorphisms
  17. Mathbox for Jim Kingdon
    1. Circle constant
    2. Number theory
    3. Real numbers
  18. Mathbox for ML
    1. Miscellaneous
    2. Cartesian exponentiation
    3. Topology
  19. Mathbox for Wolf Lammen
    1. wl-section-prop
    2. ax-luk1
    3. ax-luk2
    4. ax-luk3
    5. 1. Bootstrapping
    6. Implication chains
    7. Theorems around the conditional operator
    8. Alternative development of hadd, cadd
    9. An alternative axiom ~ ax-13
    10. Other stuff
  20. Mathbox for Brendan Leahy
    1. rabiun
    2. iundif1
    3. imadifss
    4. cureq
    5. unceq
    6. curf
    7. uncf
    8. curfv
    9. uncov
    10. curunc
    11. unccur
    12. phpreu
    13. finixpnum
    14. fin2solem
    15. fin2so
    16. ltflcei
    17. leceifl
    18. sin2h
    19. cos2h
    20. tan2h
    21. lindsadd
    22. lindsdom
    23. lindsenlbs
    24. matunitlindflem1
    25. matunitlindflem2
    26. matunitlindf
    27. ptrest
    28. ptrecube
    29. poimirlem1
    30. poimirlem2
    31. poimirlem3
    32. poimirlem4
    33. poimirlem5
    34. poimirlem6
    35. poimirlem7
    36. poimirlem8
    37. poimirlem9
    38. poimirlem10
    39. poimirlem11
    40. poimirlem12
    41. poimirlem13
    42. poimirlem14
    43. poimirlem15
    44. poimirlem16
    45. poimirlem17
    46. poimirlem18
    47. poimirlem19
    48. poimirlem20
    49. poimirlem21
    50. poimirlem22
    51. poimirlem23
    52. poimirlem24
    53. poimirlem25
    54. poimirlem26
    55. poimirlem27
    56. poimirlem28
    57. poimirlem29
    58. poimirlem30
    59. poimirlem31
    60. poimirlem32
    61. poimir
    62. broucube
    63. heicant
    64. opnmbllem0
    65. mblfinlem1
    66. mblfinlem2
    67. mblfinlem3
    68. mblfinlem4
    69. ismblfin
    70. ovoliunnfl
    71. ex-ovoliunnfl
    72. voliunnfl
    73. volsupnfl
    74. mbfresfi
    75. mbfposadd
    76. cnambfre
    77. dvtanlem
    78. dvtan
    79. itg2addnclem
    80. itg2addnclem2
    81. itg2addnclem3
    82. itg2addnc
    83. itg2gt0cn
    84. ibladdnclem
    85. ibladdnc
    86. itgaddnclem1
    87. itgaddnclem2
    88. itgaddnc
    89. iblsubnc
    90. itgsubnc
    91. iblabsnclem
    92. iblabsnc
    93. iblmulc2nc
    94. itgmulc2nclem1
    95. itgmulc2nclem2
    96. itgmulc2nc
    97. itgabsnc
    98. itggt0cn
    99. ftc1cnnclem
    100. ftc1cnnc
    101. ftc1anclem1
    102. ftc1anclem2
    103. ftc1anclem3
    104. ftc1anclem4
    105. ftc1anclem5
    106. ftc1anclem6
    107. ftc1anclem7
    108. ftc1anclem8
    109. ftc1anc
    110. ftc2nc
    111. asindmre
    112. dvasin
    113. dvacos
    114. dvreasin
    115. dvreacos
    116. areacirclem1
    117. areacirclem2
    118. areacirclem3
    119. areacirclem4
    120. areacirclem5
    121. areacirc
  21. Mathbox for Jeff Madsen
    1. Logic and set theory
    2. Real and complex numbers; integers
    3. Sequences and sums
    4. Topology
    5. Metric spaces
    6. Continuous maps and homeomorphisms
    7. Boundedness
    8. Isometries
    9. Heine-Borel Theorem
    10. Banach Fixed Point Theorem
    11. Euclidean space
    12. Intervals (continued)
    13. Operation properties
    14. Groups and related structures
    15. Group homomorphism and isomorphism
    16. Rings
    17. Division Rings
    18. Ring homomorphisms
    19. Commutative rings
    20. Ideals
    21. Prime rings and integral domains
    22. Ideal generators
  22. Mathbox for Giovanni Mascellani
    1. Tools for automatic proof building
    2. Tseitin axioms
    3. Equality deductions
    4. Miscellanea
  23. Mathbox for Peter Mazsa
    1. Notations
    2. Preparatory theorems
    3. Range Cartesian product
    4. Cosets by ` R `
    5. Relations
    6. Subset relations
    7. Reflexivity
    8. Converse reflexivity
    9. Symmetry
    10. Reflexivity and symmetry
    11. Transitivity
    12. Equivalence relations
    13. Redundancy
    14. Domain quotients
    15. Equivalence relations on domain quotients
    16. Functions
    17. Disjoints vs. converse functions
  24. Mathbox for Rodolfo Medina
    1. Partitions
  25. Mathbox for Norm Megill
    1. Predicate calculus with equality: Older axiomatization (1 rule, 14 schemes)
    2. Obsolete schemes ax-c4,c5,c7,c10,c11,c11n,c15,c9,c14,c16
    3. Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old
    4. Legacy theorems using obsolete axioms
    5. Experiments with weak deduction theorem
    6. Miscellanea
    7. Atoms, hyperplanes, and covering in a left vector space (or module)
    8. Functionals and kernels of a left vector space (or module)
    9. Opposite rings and dual vector spaces
    10. Ortholattices and orthomodular lattices
    11. Atomic lattices with covering property
    12. Hilbert lattices
    13. Projective geometries based on Hilbert lattices
    14. Construction of a vector space from a Hilbert lattice
    15. Construction of involution and inner product from a Hilbert lattice
  26. Mathbox for metakunt
    1. General helpful statements
    2. Some gcd and lcm results
    3. Least common multiple inequality theorem
    4. Logarithm inequalities
    5. Miscellaneous results for AKS formalisation
    6. Sticks and stones
    7. Permutation results
    8. Unused lemmas scheduled for deletion
  27. Mathbox for Steven Nguyen
    1. Miscellaneous theorems
    2. Utility theorems
    3. Structures
    4. Arithmetic theorems
    5. Exponents and divisibility
    6. Real subtraction
    7. Projective spaces
    8. Basic reductions for Fermat's Last Theorem
  28. Mathbox for Igor Ieskov
    1. binom2d
    2. cu3addd
    3. sqnegd
    4. negexpidd
    5. rexlimdv3d
    6. 3cubeslem1
    7. 3cubeslem2
    8. 3cubeslem3l
    9. 3cubeslem3r
    10. 3cubeslem3
    11. 3cubeslem4
    12. 3cubes
  29. Mathbox for Larry Lesyna
  30. Mathbox for OpenAI
    1. rntrclfvOAI
  31. Mathbox for Stefan O'Rear
    1. Additional elementary logic and set theory
    2. Additional theory of functions
    3. Additional topology
    4. Characterization of closure operators. Kuratowski closure axioms
    5. Algebraic closure systems
    6. Miscellanea 1. Map utilities
    7. Miscellanea for polynomials
    8. Multivariate polynomials over the integers
    9. Miscellanea for Diophantine sets 1
    10. Diophantine sets 1: definitions
    11. Diophantine sets 2 miscellanea
    12. Diophantine sets 2: union and intersection. Monotone Boolean algebra
    13. Diophantine sets 3: construction
    14. Diophantine sets 4 miscellanea
    15. Diophantine sets 4: Quantification
    16. Diophantine sets 5: Arithmetic sets
    17. Diophantine sets 6: reusability. renumbering of variables
    18. Pigeonhole Principle and cardinality helpers
    19. A non-closed set of reals is infinite
    20. Lagrange's rational approximation theorem
    21. Pell equations 1: A nontrivial solution always exists
    22. Pell equations 2: Algebraic number theory of the solution set
    23. Pell equations 3: characterizing fundamental solution
    24. Logarithm laws generalized to an arbitrary base
    25. Pell equations 4: the positive solution group is infinite cyclic
    26. X and Y sequences 1: Definition and recurrence laws
    27. Ordering and induction lemmas for the integers
    28. X and Y sequences 2: Order properties
    29. Congruential equations
    30. Alternating congruential equations
    31. Additional theorems on integer divisibility
    32. X and Y sequences 3: Divisibility properties
    33. X and Y sequences 4: Diophantine representability of Y
    34. X and Y sequences 5: Diophantine representability of X, ^, _C
    35. Uncategorized stuff not associated with a major project
    36. More equivalents of the Axiom of Choice
    37. Finitely generated left modules
    38. Noetherian left modules I
    39. Addenda for structure powers
    40. Every set admits a group structure iff choice
    41. Noetherian rings and left modules II
    42. Hilbert's Basis Theorem
    43. Additional material on polynomials [DEPRECATED]
    44. Degree and minimal polynomial of algebraic numbers
    45. Algebraic integers I
    46. The determinant / matrix adjugate/adjunct
    47. Endomorphism algebra
    48. The class equation
    49. Cyclic groups and order
    50. Cyclotomic polynomials
    51. Wedderburn's little theorem
    52. Hybrid categories proposal
    53. Miscellaneous topology
  32. Mathbox for Jon Pennant
    1. iocunico
    2. iocinico
    3. iocmbl
    4. cnioobibld
    5. arearect
    6. areaquad
  33. Mathbox for Richard Penner
    1. Short Studies
    2. Additional statements on relations and subclasses
    3. Propositions from _Begriffsschrift_
    4. Exploring Topology via Seifert and Threlfall
    5. Exploring Higher Homotopy via Kerodon
  34. Mathbox for Stanislas Polu
    1. inductionexd
    2. IMO Problems
    3. INT Inequalities Proof Generator
    4. N-Digit Addition Proof Generator
    5. AM-GM (for k = 2,3,4)
  35. Mathbox for Rohan Ridenour
    1. Misc
    2. Monoid rings
    3. Shorter primitive equivalent of ax-groth
  36. Mathbox for Steve Rodriguez
    1. Miscellanea
    2. Ratio test for infinite series convergence and divergence
    3. Multiples
    4. Function operations
    5. Calculus
    6. The generalized binomial coefficient operation
    7. Binomial series
  37. Mathbox for Andrew Salmon
    1. Principia Mathematica * 10
    2. Principia Mathematica * 11
    3. Predicate Calculus
    4. Principia Mathematica * 13 and * 14
    5. Set Theory
    6. Arithmetic
    7. Geometry
  38. Mathbox for Alan Sare
    1. Auxiliary theorems for the Virtual Deduction tool
    2. Supplementary unification deductions
    3. Conventional Metamath proofs, some derived from VD proofs
    4. What is Virtual Deduction?
    5. Virtual Deduction Theorems
    6. Theorems proved using Virtual Deduction
    7. Theorems proved using Virtual Deduction with mmj2 assistance
    8. Virtual Deduction transcriptions of textbook proofs
    9. Theorems proved using conjunction-form Virtual Deduction
    10. Theorems with a VD proof in conventional notation derived from a VD proof
    11. Theorems with a proof in conventional notation derived from a VD proof
  39. Mathbox for Glauco Siliprandi
    1. Miscellanea
    2. Functions
    3. Ordering on real numbers - Real and complex numbers basic operations
    4. Real intervals
    5. Finite sums
    6. Finite multiplication of numbers and finite multiplication of functions
    7. Limits
    8. Trigonometry
    9. Continuous Functions
    10. Derivatives
    11. Integrals
    12. Stone Weierstrass theorem - real version
    13. Wallis' product for π
    14. Stirling's approximation formula for ` n ` factorial
    15. Dirichlet kernel
    16. Fourier Series
    17. e is transcendental
    18. n-dimensional Euclidean space
    19. Basic measure theory
  40. Mathbox for Saveliy Skresanov
    1. Ceva's theorem
    2. Simple groups
  41. Mathbox for Jarvin Udandy
    1. hirstL-ax3
    2. ax3h
    3. aibandbiaiffaiffb
    4. aibandbiaiaiffb
    5. notatnand
    6. aistia
    7. aisfina
    8. bothtbothsame
    9. bothfbothsame
    10. aiffbbtat
    11. aisbbisfaisf
    12. axorbtnotaiffb
    13. aiffnbandciffatnotciffb
    14. axorbciffatcxorb
    15. aibnbna
    16. aibnbaif
    17. aiffbtbat
    18. astbstanbst
    19. aistbistaandb
    20. aisbnaxb
    21. atbiffatnnb
    22. bisaiaisb
    23. atbiffatnnbalt
    24. abnotbtaxb
    25. abnotataxb
    26. conimpf
    27. conimpfalt
    28. aistbisfiaxb
    29. aisfbistiaxb
    30. aifftbifffaibif
    31. aifftbifffaibifff
    32. atnaiana
    33. ainaiaandna
    34. abcdta
    35. abcdtb
    36. abcdtc
    37. abcdtd
    38. abciffcbatnabciffncba
    39. abciffcbatnabciffncbai
    40. nabctnabc
    41. jabtaib
    42. onenotinotbothi
    43. twonotinotbothi
    44. clifte
    45. cliftet
    46. clifteta
    47. cliftetb
    48. confun
    49. confun2
    50. confun3
    51. confun4
    52. confun5
    53. plcofph
    54. pldofph
    55. plvcofph
    56. plvcofphax
    57. plvofpos
    58. mdandyv0
    59. mdandyv1
    60. mdandyv2
    61. mdandyv3
    62. mdandyv4
    63. mdandyv5
    64. mdandyv6
    65. mdandyv7
    66. mdandyv8
    67. mdandyv9
    68. mdandyv10
    69. mdandyv11
    70. mdandyv12
    71. mdandyv13
    72. mdandyv14
    73. mdandyv15
    74. mdandyvr0
    75. mdandyvr1
    76. mdandyvr2
    77. mdandyvr3
    78. mdandyvr4
    79. mdandyvr5
    80. mdandyvr6
    81. mdandyvr7
    82. mdandyvr8
    83. mdandyvr9
    84. mdandyvr10
    85. mdandyvr11
    86. mdandyvr12
    87. mdandyvr13
    88. mdandyvr14
    89. mdandyvr15
    90. mdandyvrx0
    91. mdandyvrx1
    92. mdandyvrx2
    93. mdandyvrx3
    94. mdandyvrx4
    95. mdandyvrx5
    96. mdandyvrx6
    97. mdandyvrx7
    98. mdandyvrx8
    99. mdandyvrx9
    100. mdandyvrx10
    101. mdandyvrx11
    102. mdandyvrx12
    103. mdandyvrx13
    104. mdandyvrx14
    105. mdandyvrx15
    106. H15NH16TH15IH16
    107. dandysum2p2e4
    108. mdandysum2p2e4
  42. Mathbox for Adhemar
    1. adh-jarrsc
    2. Minimal implicational calculus
  43. Mathbox for Alexander van der Vekens
    1. General auxiliary theorems (1)
    2. Alternative for Russell's definition of a description binder
    3. Double restricted existential uniqueness
    4. Alternative definitions of function and operation values
    5. Alternative definitions of function values (2)
    6. General auxiliary theorems (2)
    7. Preimages of function values
    8. Partitions of real intervals
    9. Shifting functions with an integer range domain
    10. Words over a set (extension)
    11. Unordered pairs
    12. Number theory (extension)
    13. Even and odd numbers
    14. Number theory (extension 2)
    15. Graph theory (extension)
    16. Monoids (extension)
    17. Magmas and internal binary operations (alternate approach)
    18. Categories (extension)
    19. Rings (extension)
    20. Basic algebraic structures (extension)
    21. Linear algebra (extension)
    22. Complexity theory
    23. Elementary geometry (extension)
  44. Mathbox for Zhi Wang
    1. Propositional calculus
    2. Predicate calculus with equality
    3. ZF Set Theory - start with the Axiom of Extensionality
    4. ZF Set Theory - add the Axiom of Replacement
    5. ZF Set Theory - add the Axiom of Power Sets
    6. ZF Set Theory - add the Axiom of Union
    7. Order sets
    8. Moore spaces
    9. Topology
    10. Preordered sets and directed sets using extensible structures
    11. Posets and lattices using extensible structures
    12. Categories
    13. Examples of categories
  45. Mathbox for Emmett Weisz
    1. Miscellaneous Theorems
    2. Set Recursion
    3. Construction of Games and Surreal Numbers
  46. Mathbox for David A. Wheeler
    1. Simplify propositional expressions
    2. Natural deduction
    3. Greater than, greater than or equal to.
    4. Hyperbolic trigonometric functions
    5. Reciprocal trigonometric functions (sec, csc, cot)
    6. Identities for "if"
    7. Other functions
    8. Logarithms generalized to arbitrary base using ` logb `
    9. Logarithm laws generalized to an arbitrary base - log_
    10. Gottlob Frege's work: _Begriffsschrift_ and _Grundgesetze der Arithmetik_
    11. Formally define notions such as reflexivity
    12. Algebra helpers
    13. Algebra helper examples
    14. Formal methods "surprises"
    15. Allsome quantifier
    16. Miscellaneous
    17. Theorems about algebraic numbers
    18. Other results
    19. Examples
  47. Mathbox for Kunhao Zheng
    1. Weighted AM-GM inequality
  48. Mathbox for Ender Ting
    1. Increasing sequences and subsequences