equal
deleted
inserted
replaced
1 section \<open>Winding Numbers\<close> |
1 section \<open>Winding Numbers\<close> |
2 |
2 |
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2017)\<close> |
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2017)\<close> |
4 |
4 |
5 theory Winding_Numbers |
5 theory Winding_Numbers |
6 imports Polytope Jordan_Curve Riemann_Mapping |
6 imports |
|
7 Polytope |
|
8 Jordan_Curve |
|
9 Riemann_Mapping |
7 begin |
10 begin |
8 |
11 |
9 lemma simply_connected_inside_simple_path: |
12 lemma simply_connected_inside_simple_path: |
10 fixes p :: "real \<Rightarrow> complex" |
13 fixes p :: "real \<Rightarrow> complex" |
11 shows "simple_path p \<Longrightarrow> simply_connected(inside(path_image p))" |
14 shows "simple_path p \<Longrightarrow> simply_connected(inside(path_image p))" |