OMDoc/knowledge representation

From MathWeb

How can mathematical concepts be modeled directly in OMDoc, i.e. without modeling statements or theories about them?

Generalization

Is there "generalization" in OMDoc? -- Michael Kohlhase: Yes, for theories (via theory inclusions). But: Is an example a theory?

In OMDoc, we can express statements about mathematics, but not mathematical objects in itself. So how can we express "all diffable functions are cont." in OMDoc?

Yes, one way (easy to understand the mathematics, hard to read off from it):
1. symbol $\mathcal{C}^1$ (for interpretation: identify this with "the set of diffable functions")
2. its definition
3. symbol $\mathcal{C}^0$ (for interpretation: identify this with "the set of continuous functions")
4. its definition (e.g. $ε / δ$ )
5. theorem: $\mathcal{C}^1\subset\mathcal{C}^0$
6. its proof
Another way (harder to understand/write, easier to read off from it):
1. theory "continuous functions" (for interpretation: identify this with "the set of continuous functions")
  - ... including a symbol and a definition
2. theory "diffable functions" (for interpretation: identify this with "the set of diffable functions")
  - ... including a symbol and a definition, and the proof for the theory inclusion from diff to cont