author nipkow Tue, 05 Nov 2019 13:56:22 +0100 changeset 71031 66c025383422 parent 71028 c2465b429e6e child 71032 acedd04c1a42
tuned
 src/HOL/Analysis/Cauchy_Integral_Theorem.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Lindelof_Spaces.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Retracts.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Winding_Numbers.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Nov 05 13:56:22 2019 +0100
@@ -3,7 +3,11 @@
text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>

theory Cauchy_Integral_Theorem
-imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Retracts
+imports
+  Complex_Transcendental
+  Henstock_Kurzweil_Integration
+  Weierstrass_Theorems
+  Retracts
begin

lemma leibniz_rule_holomorphic:
@@ -4306,7 +4310,7 @@
by (auto simp: open_dist)
qed

-subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
+subsection\<open>Winding number is zero "outside" a curve\<close>

proposition winding_number_zero_in_outside:
assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)"```
```--- a/src/HOL/Analysis/Lindelof_Spaces.thy	Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy	Tue Nov 05 13:56:22 2019 +0100
@@ -1,4 +1,4 @@
-section\<open>Lindelof spaces\<close>
+section\<open>Lindel\"of spaces\<close>

theory Lindelof_Spaces
imports T1_Spaces```
```--- a/src/HOL/Analysis/Retracts.thy	Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Analysis/Retracts.thy	Tue Nov 05 13:56:22 2019 +0100
@@ -1,10 +1,12 @@
section \<open>Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\<close>

theory Retracts
-  imports Brouwer_Fixpoint Continuous_Extension Ordered_Euclidean_Space
+imports
+  Brouwer_Fixpoint
+  Continuous_Extension
+  Ordered_Euclidean_Space
begin

-
text \<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
in spaces of higher dimension.```
```--- a/src/HOL/Analysis/Winding_Numbers.thy	Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Nov 05 13:56:22 2019 +0100
@@ -3,7 +3,10 @@
text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2017)\<close>

theory Winding_Numbers
-imports Polytope Jordan_Curve Riemann_Mapping
+imports
+  Polytope
+  Jordan_Curve
+  Riemann_Mapping
begin

lemma simply_connected_inside_simple_path:```