Nicolò Cavalleri (Jun 24 2021 at 19:57): 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: Dec 21 2024 at 16:20 UTC