equal
deleted
inserted
replaced
3334 |
3334 |
3335 text\<open>We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.\<close> |
3335 text\<open>We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.\<close> |
3336 |
3336 |
3337 subsection\<open>Winding Numbers\<close> |
3337 subsection\<open>Winding Numbers\<close> |
3338 |
3338 |
3339 text\<open>The result is an integer, but it doesn't have type @{typ int}!\<close> |
|
3340 definition winding_number:: "[real \<Rightarrow> complex, complex] \<Rightarrow> complex" where |
3339 definition winding_number:: "[real \<Rightarrow> complex, complex] \<Rightarrow> complex" where |
3341 "winding_number \<gamma> z \<equiv> |
3340 "winding_number \<gamma> z \<equiv> |
3342 @n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and> |
3341 @n. \<forall>e > 0. \<exists>p. valid_path p \<and> z \<notin> path_image p \<and> |
3343 pathstart p = pathstart \<gamma> \<and> |
3342 pathstart p = pathstart \<gamma> \<and> |
3344 pathfinish p = pathfinish \<gamma> \<and> |
3343 pathfinish p = pathfinish \<gamma> \<and> |