Stream: Beginner Questions

Topic: Topology with the axiom of choice

view this post on Zulip Nicolò Cavalleri (Jun 24 2021 at 19:57):

The question I am about to ask is very weird. I am working lately with the type "'a x (('a => real) => real)" and I have a set of this type on which I have a topology. Now, I need to build a topology on the total type, "'a x (('a => real) => real)", that induces the given topology on my set. I believe there is no way to build this topology constructively, but there might be a way to prove there exists a topology satisfying my property by making use of indirect methods. Can I then put a topological_space instance on "'a x (('a => real) => real)" using SOME? Would this be problematic?

Last updated: Sep 25 2021 at 09:17 UTC