Stream: General

Topic: smooth manifold


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Aug 15 2022 at 04:16 UTC