Wouldn't that just be the function topology? http://isabelle.in.tum.de/repos/isabelle/file/2b23dd163c7f/src/HOL/Analysis/Function_Topology.thy#l553
Fabian On 4/3/2019 10:59 AM, Lawrence Paulson wrote:
Yes, I could do that. I was trying to figure out what the corresponding abstract topology should be, but failed. Such a thing must exist of course. LarryOn 3 Apr 2019, at 15:53, Fabian Immler <[email protected]> wrote: Given that there are several potential applications, I guess you could add it as a separate theory (Poly_Mapping_Normed_Vector_Space?) to HOL-Analysis?
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
