@Fabian Immler @Bohua Zhan

Is there already in your library a direct way to get the underlying topology from a manifold (a `c_manifold`

), i.e. to get a term of type `'a topology`

?

Indeed, in the context of the locale `c_manifold`

, I want to use `subtopology`

(in Abstract_Topology.thy) which requires a topology as an argument.

Yes, `subtopology carrier euclidean`

should be the topology of the manifold.

This is because the topology is already given by the type class constraint.

Yes,

`subtopology carrier euclidean`

should be the topology of the manifold.

This is because the topology is already given by the type class constraint.

Thanks.

`subtopology euclidean carrier`

works (note the order of the arguments).

Last updated: Aug 15 2022 at 04:16 UTC