[isabelle-dev] Poly_Mapping

[Fabian Immler]

Yes, of course...
I guess what I had in mind was a construction similar to the function 
topology, i.e., the topology generated by finite products of open sets.
But I didn't really think that one through, either.

Fabian


On 4/3/2019 11:03 AM, Lawrence Paulson wrote:
> No. The objects of the function topology do not have to be zero almost everywhere. Moreover, the norm for the function topology isn’t linear so you don’t get a real_normed_vector.
> Larry
> 
>> On 3 Apr 2019, at 16:01, Fabian Immler <immler at in.tum.de> wrote:
>>
>> 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.
>>> 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/52441600/attachment-0001.bin>