Vector space over continuous functions

Stream: new members

[Nicolò Cavalleri]

Oh ok I think I know an example of what you are talking about: it looks type class inference does not work very well for is_subring in the instance continuous_ring

[Nicolò Cavalleri]

In any case I guess then the file continuous_functions will be changed with definitions of subgroups instead of is_subgroup and all of this will be done over continuous bundled functions instead of the subtype of continuous functions as @Scott Morrison was suggesting

[Nicolò Cavalleri]

If I have time I can try to do it at some point

[Nicolò Cavalleri]

But for example it seems that the structure subring is not there yet so it's too early to do that

[Alex J. Best]

Theres also the possibility to use the theory of lattices with subgroup , we can set up an order on subgroups by containment (so far just like sets), and then take things like the least upper bound of two subgroups, which is the smallest subgroup containing both (the subgroup generated by their union rather than just taking the union as sets). I think that sort of thing was harder to arrange with is_subgroup.

[Kevin Buzzard]

subgroup G has a lattice structure, but the sup is not the one induced from sup on set G, as the union of two subgroups is typically not a subgroup.