[isabelle-dev] Poly_Mapping

Fabian Immler immler at in.tum.de
Wed Apr 3 17:01:46 CEST 2019

Wouldn't that just be the function topology?



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.
> Larry
>> On 3 Apr 2019, at 15:53, Fabian Immler <immler at in.tum.de> 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?

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190403/bf4132bf/attachment-0001.bin>

More information about the isabelle-dev mailing list