# [isabelle] Type classes and parameters

```Hello,

```
I am looking for a good way to express some basic mathematical objects in the current Isabelle/HOL framework.
```
```
Here is a representative example of my question. Let 'a be a compact metric space. Then a function f from 'a to real numbers is c-HÃlder continuous (where c>0 is some given positive real number) if it is continuous and
```(*_c) : sup_{x \neq y} |f(x)-f(y)|/ d(x,y)^c
```
is finite. It is easy to check that the set of c-HÃlder continuous functions is a Banach space, for the norm equal to the sup norm plus *_c.
```
In a mathematical paper, I would write this as:
```
Thm: Let X be a compact metric space, let c>0. Then the set of c-HÃlder continuous functions on X (with the above norm) is a Banach space.
```
```
My question is how to express this theorem in Isabelle/HOL in the best way using locales/type classes (given that Banach spaces are type classes). And then write conveniently statements such as: the inclusion of c-HÃlder continuous functions in d-HÃlder continuous functions is a continuous injection when d<c.
```
Any hint?

Best,
Esseger

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.