> On 4 Nov 2019, at 12:48, Manuel Eberl <[email protected]> wrote:
>
> I don't really have an idea of what material you really need for winding
> numbers. I recall that Wenda had some problems with them (about what happens
> when there's a pole on the path) – perhaps it would make sense to give that
> theory an overhaul altogether?
Our definition of winding numbers is fine to me, as it follows classic
analytical textbook definition which usually does not allow the target point on
the path. Unless we want to further generalise the definition in a topological
or algebraic direction (which does not seem too necessary at the moment), this
point-on-the-path issue is probably what we have to live with.
My two cents about our winding numbers is the organisation: winding numbers are
(kind of secretly) defined in Cauchy_Integral_Theorem.thy rather than in
Winding_Numbers.thy
<https://isabelle.in.tum.de/repos/isabelle/file/c85efa2be619/src/HOL/Analysis/Winding_Numbers.thy>,
which only contains advanced facts related to winding numbers. Maybe it is
worth having two theories about winding numbers — a basic one for the integral
theorem and an advanced one that is on the top of Jordan_Curve &
Riemann_Mapping.
Wenda
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
