[isabelle-dev] Poly_Mapping

[Lawrence Paulson]

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?
>