# [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.*