Users' Mathboxes Users' Mathboxes < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mathbox Structured version   Visualization version   GIF version

Theorem mathbox 28473
Description: (This theorem is a dummy placeholder for these guidelines. The label of this theorem, "mathbox", is hard-coded into the metamath program to identify the start of the mathbox section for web page generation.)

A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm.

For contributors:

By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm.

Mathboxes are provided to help keep your work synchronized with changes in set.mm while allowing you to work independently without affecting other contributors. Even though in a sense your mathbox belongs to you, it is still part of the shared body of knowledge contained in set.mm, and occasionally other people may make maintenance edits to your mathbox for things like keeping it synchronized with the rest of set.mm, reducing proof lengths, moving your theorems to the main part of set.mm when needed, and fixing typos or other errors. If you want to preserve it the way you left it, you can keep a local copy or keep track of the GitHub commit number.

Guidelines:

1. See conventions 26388 for our general style guidelines. For contributing via GitHub, see https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md. The metamath program command "verify markup *" will check that you have followed many of of the conventions we use.

2. If at all possible, please use only 0-ary class constants for new definitions, for example as in df-div 10434.

3. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of our indentation conventions and line wrapping.

4. All mathbox content will be on public display and should hopefully reflect the overall quality of the website.

5. Mathboxes must be independent from one another (checked by "verify markup *"). If you need a theorem from another mathbox, typically it is moved to the main part of set.mm. New users should consult with more experienced users before doing this. (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)

Hypothesis
Ref Expression
mathbox.1 𝜑
Assertion
Ref Expression
mathbox 𝜑

Proof of Theorem mathbox
StepHypRef Expression
1 mathbox.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator