Stream: General

Topic: smooth manifold

Anthony Bordg (Sep 09 2019 at 14:15):

@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.

Fabian Immler (Sep 09 2019 at 17:12):

Yes, subtopology carrier euclidean should be the topology of the manifold.
This is because the topology is already given by the type class constraint.

Anthony Bordg (Sep 09 2019 at 17:28):

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: Nov 07 2025 at 16:23 UTC