[isabelle-dev] The Great Picard Theorem

[Manuel Eberl]

I'm not an expert in complex analysis either, but do remember that it
was briefly mentioned – but not proved – in my introductory lecture on
Complex Analysis when I was an undergratuate.

My intuition tells me that this is a very beautiful result, but not one
that you need a lot, but I could be wrong about this.

I could perhaps ask around a bit.

I for one am quite open to the idea of moving more material from the
distribution to the AFP, especially from HOL-Analysis. Picard's theorem
sounds like a reasonable candidate for that, but in general, I also have
no idea where to draw the line.

Cheers,

Manuel


On 22/02/17 17:46, Lawrence Paulson wrote:
> I have just added this to the Analysis directory, making its inevitable refactoring more necessary.
> 
> Arguably it should be an AFP entry. Unfortunately, I’m not sufficiently expert in complex analysis to say whether it is core material or not. It looks like a fundamental result to me.
> 
> We should probably resolve the question of Analysis before the next release. How do we decide which things go into Complex_Main versus Analysis (which could be split into basic/advanced) and the AFP?
> 
> Larry
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>