Sorry, I think I was not being clear. What I want is making a type `CInfty`

with notation `{cinfty U -> V}`

, and ability to

- Create a substructure of
`CInfty`

later `MkCInfty`

notation to construct`{cinfty U -> V}`

from the proof that given function is C-infinity.- Ability to do [cinfty of (f \+ g)] for
`f`

,`g`

with cinfty structure. (C-infinity is also closed in addition)

In addition, I want to attach e.g.`zmodType`

on`{cinfty U -> V}`

.

`CInfty`

would not be substructure of `Linear`

, so I do not need to care about internals of `linear`

.

Sure, but you can take inspiration of how `linear`

is done to craft your `CInfty`

.

I see what you mean now. Thank you!

abab9579 has marked this topic as resolved.

Last updated: Jan 29 2023 at 16:02 UTC