Metamath Proof Explorer

Table of Contents - 20.3. Mathbox for Thierry Arnoux

  1. Propositional Calculus - misc additions
    1. bian1d
    2. or3di
    3. or3dir
    4. 3o1cs
    5. 3o2cs
    6. 3o3cs
  2. Predicate Calculus
    1. Predicate Calculus - misc additions
    2. Restricted quantification - misc additions
    3. Equality
    4. Double restricted existential uniqueness quantification
    5. Double restricted existential uniqueness quantification syntax
    6. Substitution (without distinct variables) - misc additions
    7. Existential "at most one" - misc additions
    8. Existential uniqueness - misc additions
    9. Restricted "at most one" - misc additions
  3. General Set Theory
    1. Class abstractions (a.k.a. class builders)
    2. Image Sets
    3. Set relations and operations - misc additions
    4. Unordered pairs
    5. Conditional operator - misc additions
    6. Set union
    7. Indexed union - misc additions
    8. Disjointness - misc additions
  4. Relations and Functions
    1. Relations - misc additions
    2. Functions - misc additions
    3. Operations - misc additions
    4. Explicit Functions with one or two points as a domain
    5. Isomorphisms - misc. add.
    6. Disjointness (additional proof requiring functions)
    7. First and second members of an ordered pair - misc additions
    8. Supremum - misc additions
    9. Finite Sets
    10. Countable Sets
  5. Real and Complex Numbers
    1. Complex operations - misc. additions
    2. Ordering on reals - misc additions
    3. Extended reals - misc additions
    4. Extended nonnegative integers - misc additions
    5. Real number intervals - misc additions
    6. Finite intervals of integers - misc additions
    7. Half-open integer ranges - misc additions
    8. The ` # ` (set size) function - misc additions
    9. The greatest common divisor operator - misc. add
    10. Integers
    11. Decimal numbers
  6. Decimal expansion
    1. cdp2
    2. df-dp2
    3. dp2eq1
    4. dp2eq2
    5. dp2eq1i
    6. dp2eq2i
    7. dp2eq12i
    8. dp20u
    9. dp20h
    10. dp2cl
    11. dp2clq
    12. rpdp2cl
    13. rpdp2cl2
    14. dp2lt10
    15. dp2lt
    16. dp2ltsuc
    17. dp2ltc
    18. Decimal point
    19. Division in the extended real number system
  7. Words over a set - misc additions
    1. wrdfd
    2. wrdres
    3. wrdsplex
    4. pfx1s2
    5. pfxrn2
    6. pfxrn3
    7. pfxf1
    8. s1f1
    9. s2rn
    10. s2f1
    11. s3rn
    12. s3f1
    13. s3clhash
    14. ccatf1
    15. pfxlsw2ccat
    16. wrdt2ind
    17. swrdrn2
    18. swrdrn3
    19. swrdf1
    20. swrdrndisj
    21. Splicing words (substring replacement)
    22. Cyclic shift of words
  8. Extensible Structures
    1. Structure restriction operator
    2. The opposite group
    3. Posets
    4. Complete lattices
    5. Order Theory
    6. Extended reals Structure - misc additions
    7. The extended nonnegative real numbers commutative monoid
  9. Algebra
    1. Monoids Homomorphisms
    2. Finitely supported group sums - misc additions
    3. Centralizers and centers - misc additions
    4. Totally ordered monoids and groups
    5. The symmetric group
    6. Transpositions
    7. Permutation Signs
    8. Permutation cycles
    9. The Alternating Group
    10. Signum in an ordered monoid
    11. The Archimedean property for generic ordered algebraic structures
    12. Semiring left modules
    13. Simple groups
    14. Rings - misc additions
    15. Subfields
    16. Totally ordered rings and fields
    17. Ring homomorphisms - misc additions
    18. Scalar restriction operation
    19. The commutative ring of gaussian integers
    20. The archimedean ordered field of real numbers
    21. The quotient map and quotient modules
    22. Univariate Polynomials
    23. Independent sets and families
    24. Subgroup sum / Sumset / Minkowski sum
    25. Prime Ideals
    26. Maximal Ideals
    27. The semiring of ideals of a ring
    28. The subring algebra
    29. Division Ring Extensions
    30. Vector Spaces
    31. Vector Space Dimension
  10. Field Extensions
    1. cfldext
    2. cfinext
    3. calgext
    4. cextdg
    5. df-fldext
    6. df-extdg
    7. df-finext
    8. df-algext
    9. relfldext
    10. brfldext
    11. ccfldextrr
    12. fldextfld1
    13. fldextfld2
    14. fldextsubrg
    15. fldextress
    16. brfinext
    17. extdgval
    18. fldextsralvec
    19. extdgcl
    20. extdggt0
    21. fldexttr
    22. fldextid
    23. extdgid
    24. extdgmul
    25. finexttrb
    26. extdg1id
    27. extdg1b
    28. fldextchr
    29. ccfldsrarelvec
    30. ccfldextdgrr
  11. Matrices
    1. Submatrices
    2. Matrix literals
    3. Laplace expansion of determinants
  12. Topology
    1. Open maps
    2. Regular spaces
    3. Topology of the unit circle
    4. Refinements
    5. Open cover refinement property
    6. Lindelöf spaces
    7. Paracompact spaces
    8. Pseudometrics
    9. Continuity - misc additions
    10. Topology of the closed unit interval
    11. Topology of ` ( RR X. RR ) `
    12. Order topology - misc. additions
    13. Continuity in topological spaces - misc. additions
    14. Topology of the extended nonnegative real numbers ordered monoid
    15. Limits - misc additions
    16. Univariate polynomials
  13. Uniform Stuctures and Spaces
    1. Hausdorff uniform completion
  14. Topology and algebraic structures
    1. The norm on the ring of the integer numbers
    2. Topological ` ZZ ` -modules
    3. Canonical embedding of the field of the rational numbers into a division ring
    4. Canonical embedding of the real numbers into a complete ordered field
    5. Embedding from the extended real numbers into a complete lattice
    6. Canonical embeddings into the ordered field of the real numbers
    7. Topological Manifolds
  15. Real and complex functions
    1. Integer powers - misc. additions
    2. Indicator Functions
    3. Extended sum
  16. Mixed Function/Constant operation
    1. cofc
    2. df-ofc
    3. ofceq
    4. ofcfval
    5. ofcval
    6. ofcfn
    7. ofcfeqd2
    8. ofcfval3
    9. ofcf
    10. ofcfval2
    11. ofcfval4
    12. ofcc
    13. ofcof
  17. Abstract measure
    1. Sigma-Algebra
    2. Generated sigma-Algebra
    3. lambda and pi-Systems, Rings of Sets
    4. The Borel algebra on the real numbers
    5. Product Sigma-Algebra
    6. Measures
    7. The counting measure
    8. The Lebesgue measure - misc additions
    9. The Dirac delta measure
    10. The 'almost everywhere' relation
    11. Measurable functions
    12. Borel Algebra on ` ( RR X. RR ) `
    13. Caratheodory's extension theorem
    14. Caratheodory's extension theorem: examples and applications
    15. Caratheodory's extension theorem: measure on RR ^ N
  18. Integration
    1. Lebesgue integral - misc additions
    2. Bochner integral
  19. Euler's partition theorem
    1. oddpwdc
    2. oddpwdcv
    3. eulerpartlemsv1
    4. eulerpartlemelr
    5. eulerpartlemsv2
    6. eulerpartlemsf
    7. eulerpartlems
    8. eulerpartlemsv3
    9. eulerpartlemgc
    10. eulerpartleme
    11. eulerpartlemv
    12. eulerpartlemo
    13. eulerpartlemd
    14. eulerpartlem1
    15. eulerpartlemb
    16. eulerpartlemt0
    17. eulerpartlemf
    18. eulerpartlemt
    19. eulerpartgbij
    20. eulerpartlemgv
    21. eulerpartlemr
    22. eulerpartlemmf
    23. eulerpartlemgvv
    24. eulerpartlemgu
    25. eulerpartlemgh
    26. eulerpartlemgf
    27. eulerpartlemgs2
    28. eulerpartlemn
    29. eulerpart
  20. Sequences defined by strong recursion
    1. csseq
    2. df-sseq
    3. subiwrd
    4. subiwrdlen
    5. iwrdsplit
    6. sseqval
    7. sseqfv1
    8. sseqfn
    9. sseqmw
    10. sseqf
    11. sseqfres
    12. sseqfv2
    13. sseqp1
  21. Fibonacci Numbers
    1. cfib
    2. df-fib
    3. fiblem
    4. fib0
    5. fib1
    6. fibp1
    7. fib2
    8. fib3
    9. fib4
    10. fib5
    11. fib6
  22. Probability
    1. Probability Theory
    2. Conditional Probabilities
    3. Real-valued Random Variables
    4. Preimage set mapping operator
    5. Distribution Functions
    6. Cumulative Distribution Functions
    7. Probabilities - example
    8. Bertrand's Ballot Problem
  23. Signum (sgn or sign) function - misc. additions
    1. sgncl
    2. sgnclre
    3. sgnneg
    4. sgn3da
    5. sgnmul
    6. sgnmulrp2
    7. sgnsub
    8. sgnnbi
    9. sgnpbi
    10. sgn0bi
    11. sgnsgn
    12. sgnmulsgn
    13. sgnmulsgp
    14. fzssfzo
    15. gsumncl
    16. gsumnunsn
    17. Operations on words
  24. Polynomials with real coefficients - misc additions
    1. plymul02
    2. plymulx0
    3. plymulx
    4. plyrecld
    5. signsplypnf
    6. signsply0
  25. Descartes's rule of signs
    1. Sign changes in a word over real numbers
    2. Counting sign changes in a word over real numbers
    3. Sign changes in a polynomial with real coefficients
  26. Number Theory
    1. efcld
    2. iblidicc
    3. rpsqrtcn
    4. divsqrtid
    5. cxpcncf1
    6. efmul2picn
    7. fct2relem
    8. ftc2re
    9. fdvposlt
    10. fdvneggt
    11. fdvposle
    12. fdvnegge
    13. prodfzo03
    14. actfunsnf1o
    15. actfunsnrndisj
    16. itgexpif
    17. fsum2dsub
    18. Representations of a number as sums of integers
    19. Vinogradov Trigonometric Sums and the Circle Method
    20. The Ternary Goldbach Conjecture: Final Statement
  27. Elementary Geometry
    1. Two-dimensional geometry
    2. Morley's Miracle
    3. Outer Five Segment (not used, no need to move to main)
  28. LeftPad Project
    1. clpad
    2. df-lpad
    3. lpadval
    4. lpadlem1
    5. lpadlem3
    6. lpadlen1
    7. lpadlem2
    8. lpadlen2
    9. lpadmax
    10. lpadleft
    11. lpadright